Skip to main content

Research Repository

See what's under the surface

Advanced Search

On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner

Dennis, Louise Abigail; Jamnik, Mateja; Pollet, Martin

Authors

Louise Abigail Dennis

Mateja Jamnik

Martin Pollet



Contributors

Jacques Carette
Editor

William Farmer
Editor

Abstract

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.

Publication Date Jan 1, 2005
Publisher Elsevier
Peer Reviewed Peer Reviewed
APA6 Citation Dennis, L. A., Jamnik, M., & Pollet, M. (2005). On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner. In W. Farmer, & J. Carette (Eds.),
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf
Additional Information To be published in the Electronic Notes in Computer Science (ENTCS) series.

Files

comp_pp_final.pdf (176 Kb)
PDF

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





You might also like



Downloadable Citations

;