Re: [isabelle] proof dags?

Matej ( 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

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