Re: [isabelle] proof dags?



On Sat, 2 Jun 2012, John Wickerson wrote:

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.

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.