- Abstract:
-
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.
- Links To Paper
- SpringerLink
- Personal Page
- Bibtex format
- @InProceedings{EDI-INF-RR-0483,
- author = {
Lucas Dixon
and Jacques Fleuriot
},
- title = {IsaPlanner: A Prototype Proof Planner in Isabelle},
- book title = {Proceedings of CADE 2003 (Conference on Automated Deduction)},
- publisher = {Springer},
- year = 2003,
- month = {Jul},
- volume = {2741},
- pages = {279-283},
- doi = {10.1007/b11829},
- url = {http://www.springerlink.com/link.asp?id=4numwr9n562dmmyj},
- }
|
