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...

Full description

Bibliographic Details
Main Authors: Dennis, Louise Abigail, Jamnik, Mateja, Pollet, Martin
Other Authors: Carette, Jacques
Format: Conference or Workshop Item
Published: Elsevier 2005
Online Access:https://eprints.nottingham.ac.uk/298/