Abstract
This paper analyzes the effect of heuristic search algorithms like A* and IDA* to accelerate proof-state based theorem provers. A functional implementation of possibly weighted A* is proposed that extends Dijkstra’s single-source shortest-path algorithm. Efficient implementation issues and possible flaws for both A* and IDA* are discussed in detail.
Initial results with first and higher order logic examples in Isabelle indicate that directed automated theorem proving is superior to other known general inference mechanisms and that it can enhance other proof techniques like model elimination.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Allen, J. Hendler, and A. Tate, editors. Readings in Planning. Morgan Kaufmann, 1990.
F. Bacchus and F. Kabanza. Using temporal logics to express search control knowledge for planning. Artificial Intelligence, 116:123–191, 2000.
B. Barras, S. Boutin, C. Cornes, J. Courant, J. C. Filliatre, E. Giménez, H. Herbelin, G. Huet, C. Munoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual-Version V6.1. Technical Report 0203, INRIA, 1997.
D. Basin and H. Ganzinger. Automated complexity analysis based on ordered resolution. Journal of the ACM, 48(1):70–109, 2001.
G. S. Brodal and C. Okasaki. Optimal purely functional priority queues. Journal of Functional Programming, 6(6):839–857, 1996.
E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
E. W. Dijkstra. A note on two problems in connection with graphs. Numerische Mathematik, 1:269–271, 1959.
W. Dowling and J. Gallier. Linear-time algorithms for testing the satisfiability of propositional horn formulae. Journal of Logic Programming, 3:267–284, 1984.
S. Edelkamp. Planning with pattern databases. In European Conference on Planning (ECP), Lecture Notes in Computer Science. Springer, 2001. 13–24.
S. Edelkamp, A. Lluch-Lafuente, and S. Leue. Protocol verification with heuristic search. In AAAI-Spring Symposium on Model-based Validation of Intelligence, pages 75–83, 2001.
M. L. Fredman and R. E. Tarjan. Fibonacci heaps and their uses in improved network optimization algorithm. Journal of the ACM, 34(3):596–615, 1987.
M. Genesereth and N. Nilsson. Logical Foundations of Artificial Intelligence. Morgan Kaufmann, 1987.
M. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis. Kluwer, 1987.
J. Harrison. Optimizing proof search in model elimination. In Conference on Automated Deduction (CADE), pages 313–327, 1996.
P. E. Hart, N. J. Nilsson, and B. Raphael. A formal basis for heuristic determination of minimum path cost. IEEE Trans. on SSC, 4:100, 1968.
M. Helmert. Decidability and undecidability results for planning with numerical state variables. In Artificial Intelligence Planning and Scheduling (AIPS), 2002.
T. A. Henzinger, P. W. A. Puri, and P. Varaiya. What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57:94–124, 1998.
J. Hoffmann and B. Nebel. The FF planning system: Fast plan generation through heuristic search. Journal of Artificial Research (JAIR), 14:253–302, 2001.
R. E. Korf. Linear-space best-first search. Artificial Intelligence, 62(1):41–78, 1993.
R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A high-performance theorem prover. Journal of Automated Reasoning, 8(2):183–212, Apr. 1992.
D. W. Loveland. Theorem-provers combining model elimination and resolution. In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pages 73–86. University Press, Edinburgh, 1969.
T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
C. Okasaki. Purely Functional Data Structures, chapter 3. Cambridge University Press, 1998.
S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas. PVS: Combining specification, proof checking, and model checking. In Computer-Aided Verification (CAV), Lecture Notes in Computer Science, pages 411–414. Springer, 1996.
L. C. Paulson. Strategic principles in the design of Isabelle. In Proceedings of the CADE Workshop on Strategies in Automated Deduction, pages 11–16, 1998.
J. Pearl. Heuristics. Addison-Wesley, 1985.
F. Reffel and S. Edelkamp. Error detection with directed symbolic model checking. In World Congress on Formal Methods (FM), Lecture Notes in Computer Science, pages 195–211. Springer, 1999.
A. Reinefeld and T. Marsland. Enhanced iterative-deepening search. IEEE Transactions on Pattern Analysis and Machine Intelligence, 16(7):701–710, 1994.
M. E. Stickel. A Prolog technology theorem prover: Implementation by an extended Prolog compiler. In Conference on Automated Deduction (CADE), volume 230, pages 573–587. Springer, 1986.
N. Voelker, 2002. Personal Communication.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Edelkamp, S., Leven, P. (2002). Directed Automated Theorem Proving. In: Baaz, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2002. Lecture Notes in Computer Science(), vol 2514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36078-6_10
Download citation
DOI: https://doi.org/10.1007/3-540-36078-6_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00010-5
Online ISBN: 978-3-540-36078-0
eBook Packages: Springer Book Archive