On the Comparison of Proof Planning Systems: , [Omega]mega and IsaPlanner

@article{citeulike:2136664, abstract = {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, [lambda]CLaM, [Omega]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.}, author = {Dennis, Louise A. and Jamnik, Mateja and Pollet, Martin }, booktitle = {Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005)}, citeulike-article-id = {2136664}, comment = {I need to read a less abstract paper first and then come back to this one.}, doi = {10.1016/j.entcs.2005.11.025}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {planning, proof}, month = {March}, number = {1}, pages = {93--110}, posted-at = {2007-12-17 14:23:02}, priority = {0}, title = {On the Comparison of Proof Planning Systems: , [Omega]mega and IsaPlanner}, url = {http://dx.doi.org/10.1016/j.entcs.2005.11.025}, volume = {151}, year = {2006} }

TY - JOUR ID - citeulike:2136664 L3 - citeulike-article-id:2136664 TI - On the Comparison of Proof Planning Systems: , [Omega]mega and IsaPlanner T2 - Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005) JF - Electronic Notes in Theoretical Computer Science VL - 151 IS - 1 SP - 93 EP - 110 N2 - 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, [lambda]CLaM, [Omega]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. KW - planning KW - proof N1 - I need to read a less abstract paper first and then come back to this one. AU - Dennis, Louise AU - Jamnik, Mateja AU - Pollet, Martin PY - 2006/03/21/ UR - http://dx.doi.org/10.1016/j.entcs.2005.11.025 ER -