- Abstract:
-
Proof planning is an approach to the automation of theorem proving in which search is conducted, not at the object-level, but among a set of proof methods. This approach dramatically reduces the amount of search but at the cost of completeness. We critically examine proof planning, identifying both its strengths and weaknesses.We use this analysis to explore ways of enhancing proof planning to overcome its current weaknesses.
- Copyright:
- 2002 by Springer. All Rights Reserved
- Links To Paper
- 1st Link
- Bibtex format
- @InBook{EDI-INF-RR-1311,
- author = {
Alan Bundy
},
- title = {A Critique of Proof Planning},
- book title = {Computational Logic: Logic Programming and Beyond. Essays in Honour of Robert A. Kowalski, Part II},
- publisher = {Springer},
- year = 2002,
- volume = {LNAI 2408},
- pages = {160-177},
- url = {http://www.springer.com/computer/artificial/book/978-3-540-43960-8},
- }
|