Automated theorem proving

Overview

David A. Plaisted

Published Online: Jan 17 2014

DOI: 10.1002/wcs.1269

Full article on Wiley Online Library: HTML PDF

Can't access this content? Tell your librarian.

Automated theorem proving is the use of computers to prove or disprove mathematical or logical statements. Such statements can express properties of hardware or software systems, or facts about the world that are relevant for applications such as natural language processing and planning. A brief introduction to propositional and first‐order logic is given, along with some of the main methods of automated theorem proving in these logics. These methods of theorem proving include resolution, Davis and Putnam‐style approaches, and others. Methods for handling the equality axioms are also presented. Methods of theorem proving in propositional logic are presented first, and then methods for first‐order logic. WIREs Cogn Sci 2014, 5:115–128. doi: 10.1002/wcs.1269 This article is categorized under: Computer Science > Artificial Intelligence Philosophy > Artificial Intelligence Philosophy > Knowledge and Belief

A semantic tree.

[ Normal View | Magnified View ]

References

Cook, SA. The complexity of theorem‐proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC `71. New York: ACM; 1971, 151–158.
Levin, LA. Universal search problems. Prob Inf Transm 1973, 9:115–116.
Davis, M, Logemann, G, Loveland, D. A machine program for theorem‐proving. Commun ACM 1962, 5:394–397.
Davis, M, Putnam, H. A computing procedure for quantification theory. J ACM 1960, 7:201–215.
D. Mitchell,, B. Selman,, and H. Levesque,. Hard and easy distributions of SAT problems. In: Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI‐92), San Jose, CA 459–465, 1992.
Malik, S, Zhang, L. Boolean satisfiability from theoretical hardness to practical success. Commun ACM 2009, 52:76–82.
Moskewicz, MW, Madigan, CF, Zhao, Y, Zhang, L, Malik, S. Chaff: engineering an efficient sat solver. In: Proceedings of the 38th annual Design Automation Conference, DAC `01. ACM; 2001, 530–535.
João, P, Silva, M, Sakallah, KA. Grasp—a new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE/ACM international conference on Computer‐aided design, ICCAD `96. IEEE Computer Society; 1996, 220–227.
Haken, A. The intractability of resolution. Theor Comput Sci 1985, 39, 297–308.
Fitting, M. First‐Order Logic and Automated Theorem Proving. New York: Springer‐Verlag; 1990.
Davis, M. Eliminating the irrelevant from machanical proofs. Proc Symp Appl Math 1963, 15:15–30.
Gilmore, PC. A proof method for quantification theory. IBM J Res Dev 1960, 4:28–35.
Lee, S‐J, Plaisted, D. Eliminating duplication with the hyper‐linking strategy. J Automat Reason 1992, 9, 25–42.
Billon, J‐P. The disconnection method. In: Miglioli, P, Moscato, U, Mundici, D, Ornaghi, M, eds. Proceedings of TABLEAUX‐96. LNAI, vol. 1071. Springer; 1996, 110–126.
G. Stenz, and R. Letz,. DCTP—a disconnection calculus theorem prover. In: Gore R, Leitsch A, Nipkow T, eds. Proceedings of the International Joint Conference on Automated Reasoning, Number 2083 in Lecture Notes in Artificial Intelligence. Springer; 2001, 381–385.
Plaisted, DA, Zhu, Y. Ordered semantic hyper linking. J Autom Reason 2000, 25:167–217.
Baumgartner, P. FDPLL—a first‐order Davis‐Putnam‐Logeman‐Loveland procedure. In: McAllester, D, ed. CADE‐17—The 17th International Conference on Automated Deduction, vol. 1831. Springer; 2000, 200–219.
Baumgartner, P, Tinelli, C. The model evolution calculus. In: Baader, F, ed. CADE‐19: The 19th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 2741. Springer; 2003, 350–364.
Ganzinger, H, Korovin, K. New directions in instantiation‐based theorem proving. In: Proceedings of 18th IEEE Symposium on Logic in Computer Science, (LICS`03). IEEE Computer Society Press; 2003, 55–64.
De Moura, L, Bjørner, N. Satisfiability modulo theories: introduction and applications. Commun ACM 2011, 54:69–77.
Robinson, J. A machine‐oriented logic based on the resolution principle. J Assoc Comput Mach 1965, 12:23–41.
Lassez, J‐L, Plotkin, G. Computational Logic: Essays in Honor of Alan Robinson. Cambridge, MA: MIT Press; 1991.
Martelli, A, Montanari, U. An efficient unification algorithm. Trans Programm Lang Syst 1982, 4:258–282.
Paterson, M, Wegman, MN. Linear unification. J Comput Syst Sci 1978, 16:158–167.
Ramakrishnan, IV, Sekar, R, Voronkov, A. Term indexing. In: Robinson, A, Voronkov, A, eds. Handbook of Automated Reasoning, vol. II Chapter 26. Amsterdam: Elsevier Science; 2001, 1853–1964.
Riazanov, A. Implementing an efficient theorem prover. PhD Thesis, The University of Manchester, Manchester, July 2003.
Bundy, A. The Computer Modelling of Mathematical Reasoning. New York: Academic Press; 1983.
Chang, C, Lee, R. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press; 1973.
Leitsch, A. The Resolution Calculus. Berlin: Springer‐Verlag; 1997 Texts in Theoretical Computer Science.
Loveland, D. Automated Theorem Proving: A Logical Basis. New York: North‐Holland; 1978.
Wos, L, Overbeek, R, Lusk, E, Boyle, J. Automated Reasoning: Introduction and Applications. Englewood Cliffs, NJ: Prentice Hall; 1984.
Loveland, D. A simplified format for the model elimination procedure. J ACM 1969, 16:349–363.
Andrews, PB. Theorem proving via general matings. J Assoc Comput Mach 1981, 28:193–214.
Hähnle, R. Tableaux and related methods. In: Robinson, A, Voronkov, A, eds. Handbook of Automated Reasoning, vol. I Chapter 3. Elsevier Science; 2001, 100–178.
Bibel, W. Automated Theorem Proving. Second ed. Braunschweig/Wiesbaden: Vieweg; 1987.
Letz, R, Stenz, G. Model elimination and connection tableau procedures. In: Robinson, A, Voronkov, A, eds. Handbook of Automated Reasoning, vol. II Chapter 28. Amsterdam: Elsevier Science; 2001, 2015–2114.
Otten, J, Bibel, W. LeanCoP: lean connection‐based theorem proving. J Symb Comput 2003, 36:139–161.
Otten, J. A non‐clausal connection calculus. In: Proceedings of the 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX`11. Springer‐Verlag; 2011, 226–241.
Nelson, G, Oppen, DC. Simplification by cooperating decision procedures. ACM TOPLAS 1979, 1:245–257.
Nelson, G, Oppen, DC. Fast decision procedures based on congruence closure. J ACM 1980, 27:356–364.
Boyer, R, Kaufmann, M, Moore, J. The Boyer‐Moore theorem prover and its interactive enhancement. Comput Math Appl 1995, 29:27–62.
Gordon, MJ, Melham, TF, eds. Introduction to HOL: A Theorem‐Proving Environment for Higher‐Order Logic. Cambridge University Press; 1993.
Owre, S, Rushby, JM, Shankar, N. PVS: a prototype verification system. In: Kapur, D, ed. 11th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 607. Springer‐Verlag; 1992, 748–752.
Paulson, LC. The foundation of a generic theorem prover. J Autom Reason 1989, 5:363–397.
Coquand, T, Huet, G. The calculus of constructions. Inf Comput 1988, 76(2–3):95–120.
Bachmair, L, Ganzinger, H, Voronkov, A. Elimination of equality via transformation with ordering constraints. Lect Notes Comput Sci 1998, 1421:175–190.
Brand, D. Proving theorems with the modification method. SIAM J Comput 1975, 4:412–430.
Dershowitz, N. Termination of rewriting. J Symb Comput 1987, 3:69–116.
Kamin, S, Levy, J‐J. Two generalizations of the recursive path ordering, Unpublished, February 1980.
Plaisted, D. A recursively defined ordering for proving termination of term rewriting systems. Technical report R‐78‐943, University of Illinois at Urbana‐Champaign, Urbana, IL, 1978.
Plaisted, D. Well‐founded orderings for proving termination of systems of rewrite rules. Technical report R‐78‐932, University of Illinois at Urbana‐Champaign, Urbana, IL, 1978.
Arts, T, Giesl, J. Termination of term rewriting using dependency pairs. Theor Comput Sci 2000, 236(1–2):133–178.
Giesl, J, Schneider‐Kamp, P, Thiemann, R. Automatic termination proofs in the dependency pair framework. In: IJCAR, 281–286, 2006.
Hirokawa, N, Middeldorp, A. Automating the dependency pair method. In: Baader, F, ed. 19th International Conference on Automated Deduction (CADE). Springer Verlag: Lecture Notes in Computer Science; 2741; 2003, 32–46.
Nieuwenhuis, R, Rubio, A. Paramodulation‐based theorem proving. In: Robinson, A, Voronkov, A, eds. Handbook of Automated Reasoning, vol. I Chapter 7. Amsterdam: Elsevier Science; 2001, 371–443.
Robinson, G, Wos, L. Paramodulation and theorem‐proving in first order theories with equality. In: Machine Intelligence, vol. 4. Edinburgh, Scotland: Edinburgh University Press; 1969, 135–150.
Bachmair, L, Ganzinger, H. Rewrite‐based equational theorem proving with selection and simplification. J Log Comput 1994, 4:217–247.
Bachmair, L, Ganzinger, H. Resolution theorem proving. In: Robinson, A, Voronkov, A, eds. Handbook of Automated Reasoning. Amsterdam: Elsevier Science; 2001, 19–99.
Bachmair, L, Ganzinger, H, Lynch, C, Snyder, W. Basic paramodulation. Inf Comput 1995, 121:172–192.
Hsiang, J, Rusinowitch, M. Proving refutational completeness of theorem‐proving strategies: the transfinite semantic tree method. J Assoc Comput Mach 1991, 38:559–587.
Nieuwenhuis, R, Rubio, A. Theorem proving with ordering and equality constrained clauses. J Symb Comput 1995, 19:321–351.
McCune, WW. Solution of the Robbins problem. JAutom Reason 1997, 19:263–276.
Knuth, DE, Bendix, PB. Simple word problems in universal algebras. In: Leech, J, ed. Computational Problems in Abstract Algebra. Oxford: Pergamon Press; 1970, 263–297.
Baader, F, Nipkow, T. Term Rewriting and All That. Cambridge, England: Cambridge University Press; 1998.
Dershowitz, N, Jouannaud, J‐P. Rewrite systems. In: van Leeuwen, J, ed. Handbook of Theoretical Computer Science. Amsterdam: North‐Holland; 1990.
Dershowitz, N, Plaisted, DA. Rewriting. In: Robinson, A, Voronkov, A, eds. Handbook of Automated Reasoning, vol. I Chapter 9. Elsevier Science; 2001, 535–610.
Ohlebusch, E. Advanced Topics in Term Rewriting. New York: Springer; 2002.
Terese. Term Rewriting Systems, Volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge: Cambridge University Press; 2003.
Armando, A, Bonacina, MP, Ranise, S, Schulz, S. New results on rewrite‐based satisfiability procedures. ACM Trans Comput Logic 2009, 10:4:1–4:51.
Fermüller, CG, Leitsch, A, Hustadt, U, Tammet, T. Handbook of Automated Reasoning. Resolution Decision Procedures, 1791–1849. Amsterdam, The Netherlands: Elsevier Science Publishers B. V.; 2001.
Kovács, L, Voronkov, A. First‐order theorem proving and Vampire. In: Proceedings of the 25th International Conference on Computer Aided Verification, CAV`13. Berlin, Heidelberg: Springer‐Verlag; 2013, 1–35.
Schulz, S. E— a brainiac theorem prover. AI Commun 2002, 15(2,3):111–126.
Weidenbach, C. Spass—version 0.49. J Autom Reason 1997, 18:247–252.
Bridge, JP, Paulson, LC. Case splitting in an automatic theorem prover for real‐valued special functions. J Autom Reason 2013, 50:99–117.

Access to this WIREs title is by subscription only.

Recommend to Your
Librarian Now!

Automated theorem proving

Browse by Topic

Access to this WIREs title is by subscription only.

The latest WIREs articles in your inbox