[isabelle] proof dags?



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




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