Email Gateway (Aug 18 2022 at 20:09): Email Gateway (Aug 18 2022 at 20:09):From: Ramana Kumar <rk436@cam.ac.uk>
Matej (http://www.cl.cam.ac.uk/~mu232/) has been working on a different but
related problem of including diagrammatic proofs (for formulae that can be
specified and proved in some diagrammatic language) within Isabelle proofs.
He might have ideas about how to make (a frontend for) Isar itself more
graphical.
Email Gateway (Aug 18 2022 at 20:13):From: John Wickerson <jpw48@cam.ac.uk>
Good idea, thanks Ramana :)
John
Email Gateway (Aug 18 2022 at 20:13):From: Makarius <makarius@sketis.net>
I have occasionally pondered the question how the implicit dependency
structure and the primary Isar text can be linked in a user interface.
This means some kind of augmented text editing as in Isabelle/jEdit with a
bit more than just a boring tree view on the side. jEdit also has notions
for drag-and-drop of text pieces and various operations on collections of
text intervals.
So one mainly needs to link existing concepts for plain text with the
structural information of the semantic document model. Advanced IDEs for
programming languages probably have something to offer here already, but I
don't know anything from first sight.
If anybody can point to examples from Eclipse, Netbeans, IntelliJ IDEA, or
even Visiual Studio, I would be interested to study them to learn how it
fits into the proof document model.
Makarius
Email Gateway (Aug 18 2022 at 20:14):From: Gudmund Grov <ggrov@staffmail.ed.ac.uk>
Dear John,
I am currently working on a graph based language to write techniques/tactics for (the Isabelle based) Isaplanner
proof planner (see http://dream.inf.ed.ac.uk/projects/isaplanner/ - although a bit out of date), but I am thinking of
ways of doing this more directly in Isabelle.
The plan is at some point to get some sort of drag and drop interface as you suggest. This is very much work
in progress, but I hope to have something working and written up in the not too distant future, which once written, I'll be
happy to send to you.
Cheers,
Gudmund
Email Gateway (Aug 18 2022 at 20:15):From: Jens Doll <jd@cococo.de>
Hello Ramana ,
a DAG is not the full picture. Proofs in general consist of forests,
i.e. several DAGs connected at different hierarchical levels. Only in
the case of axiomatic theories (Hilbert style ...) a single DAG is
sufficient.
Happy Reasoning,
Jens
Email Gateway (Aug 18 2022 at 20:26):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
It seems to me that proving a lemma in Isabelle is much like building a dag, where the facts are nodes and the implications between facts are arrows. When several nodes "line up" in a simple chain we can use the Isar construction "hence"; and for some other dag shapes the "moreover/ultimately" pattern works. But in general, one needs to invent names sometimes when the underlying proof dag doesn't conform to one of these templates.
I was wondering: has there been any work on a UI that lets the user construct this dag directly? I'm imagining a sort of drag-and-drop interface that lets me drag arrows between boxes and move boxes around a canvas, and so on.
Best wishes,
John
Last updated: Nov 21 2024 at 12:39 UTC