Re: [isabelle] proof dags?



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


On 2 Jun 2012, at 17:46, John Wickerson 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
> 


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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