On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner - Dennis, Louise Abigail; Jamnik, Mateja; Pollet, Martin (Elsevier, 2005)
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.