On the Comparison of Proof Planning Systems: , Ωmega and IsaPlanner

Louise A. Dennis, Mateja Jamnik, Martin Pollet

Research output: Contribution to journalArticlepeer-review


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, λCLaM, Ωmega 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.
Original languageEnglish
Pages (from-to)93-110
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 11 Mar 2006


Dive into the research topics of 'On the Comparison of Proof Planning Systems: , Ωmega and IsaPlanner'. Together they form a unique fingerprint.

Cite this