IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. This paper introduces our approach to proof planning, gives and overview of IsaPlanner, and presents one simple yet effective reasoning technique.
CITATION STYLE
Dixon, L., & Fleuriot, J. (2003). IsaPlanner: A prototype proof planner in Isabelle. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2741, pp. 279–283). Springer Verlag. https://doi.org/10.1007/978-3-540-45085-6_22
Mendeley helps you to discover research relevant for your work.