On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner
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 thr...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Conference or Workshop Item |
| Published: |
Elsevier
2005
|
| Online Access: | https://eprints.nottingham.ac.uk/298/ |
| _version_ | 1848790389362786304 |
|---|---|
| author | Dennis, Louise Abigail Jamnik, Mateja Pollet, Martin |
| author2 | Carette, Jacques |
| author_facet | Carette, Jacques Dennis, Louise Abigail Jamnik, Mateja Pollet, Martin |
| author_sort | Dennis, Louise Abigail |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T18:11:50Z |
| format | Conference or Workshop Item |
| id | nottingham-298 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:50Z |
| publishDate | 2005 |
| publisher | Elsevier |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-2982020-05-04T20:30:46Z https://eprints.nottingham.ac.uk/298/ 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. Elsevier Carette, Jacques Farmer, William 2005 Conference or Workshop Item PeerReviewed Dennis, Louise Abigail, Jamnik, Mateja and Pollet, Martin (2005) On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner. In: 12th Symposium on the Integratoin of Symbolic Computation and Mechanized Reasoning (Calculemus 2005), July, Newcastle. (In Press) |
| spellingShingle | Dennis, Louise Abigail Jamnik, Mateja Pollet, Martin On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner |
| title | On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner |
| title_full | On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner |
| title_fullStr | On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner |
| title_full_unstemmed | On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner |
| title_short | On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner |
| title_sort | on the comparison of proof planning systems: lambda-clam, omega and isaplanner |
| url | https://eprints.nottingham.ac.uk/298/ |