Louise Abigail Dennis
On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner
Dennis, Louise Abigail; Jamnik, Mateja; Pollet, Martin
Authors
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.
Citation
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 | Mar 28, 2024 |
Publisher | Elsevier |
Peer Reviewed | Peer Reviewed |
Public URL | https://nottingham-repository.worktribe.com/output/1020262 |
Additional Information | To be published in the Electronic Notes in Computer Science (ENTCS) series. |
Files
comp_pp_final.pdf
(176 Kb)
PDF
You might also like
The intellectual structure of game research
(2018)
Journal Article
Experimental study of the short-circuit performance for a 600V normally-off p-gate GaN HEMT
(2017)
Conference Proceeding
Electrical and thermal failure modes of 600 V p-gate GaN HEMTs
(2017)
Journal Article
An interdisciplinary review of energy storage for communities: challenges and perspectives
(2017)
Journal Article
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: digital-library-support@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search