Open AccessOn the Comparison of Proof Planning Systems: , Ωmega and IsaPlanner
Author(s) -
Louise A. Dennis,
Mateja Jamnik,
Martin Pollet
Publication year - 2006
Publication title -
electronic notes in theoretical computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.242
H-Index - 60
ISSN - 1571-0661
DOI - 10.1016/j.entcs.2005.11.025
Subject(s) - proof of concept , burden of proof , direct proof , computer science , computer assisted proof , key (lock) , proof complexity , analytic proof , structural proof theory , mega , constructive proof , control (management) , proof theory , theoretical computer science , mathematical proof , mathematics , automated theorem proving , artificial intelligence , programming language , discrete mathematics , physics , geometry , computer security , astronomy , political science , law , operating system
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
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom