Louise Abigail Dennis
On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner
Dennis, Louise Abigail; Jamnik, Mateja; Pollet, Martin
We present a framework for describing proof planners. This framework is based around a decomposition of proof planners into planning states, proof language, proof plans, proof methods, proof revision, proof control and planning algorithms.
We use this framework to motivate the comparison of three recent proof planning systems, lclam, OMEGA and IsaPlanner, and demonstrate how the framework allows us to discuss and illustrate both their similarities and differences in a consistent fashion. This analysis reveals that proof control and the use of contextual information in planning states are key areas in need of further investigation.
Dennis, L. A., Jamnik, M., & Pollet, M. (2005). On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner. In J. Carette, & W. Farmer (Eds.),
|Conference Name||12th Symposium on the Integratoin of Symbolic Computation and Mechanized Reasoning (Calculemus 2005)|
|Publication Date||Jan 1, 2005|
|Deposit Date||Nov 14, 2005|
|Publicly Available Date||Oct 9, 2007|
|Peer Reviewed||Peer Reviewed|
|Additional Information||To be published in the Electronic Notes in Computer Science (ENTCS) series.|
You might also like
Making science public: challenges and opportunities
Constructing notions of healthcare productivity: The call for a new professionalism?
Association between surgeon special interest and mortality after emergency laparotomy
The Dalton quantum chemistry program system
Embodiment in skateboarding videogames