Re: [isabelle] proof dags?



Good idea, thanks Ramana :)

John

On 3 Jun 2012, at 16:10, Ramana Kumar wrote:

> 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.
> 
> On Sat, Jun 2, 2012 at 5:46 PM, John Wickerson <jpw48 at cam.ac.uk> wrote:
> 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.