Top

Published in:

2015 | OriginalPaper | Chapter

History and Prospects for First-Order Automated Deduction

Author : David A. Plaisted

Published in: Automated Deduction - CADE-25

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

On the fiftieth anniversary of the appearance of Robinson’s resolution paper [57], it is appropriate to consider the history and status of theorem proving, as well as its possible future directions. Here we discuss the history of first-order theorem proving both before and after 1965, with some personal reflections. We then generalize model-based reasoning to first-order provers, and discuss what it means for a prover to be goal sensitive. We also present a way to analyze asymptotically the size of the search space of a first-order prover in terms of the size of a minimal unsatisfiable set of ground instances of a set of first-order clauses.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

next chapter Stumbling Around in the Dark: Lessons from Everyday Mathematics

Andrews, P.: Theorem proving via general matings. J. ACM 28, 193–214 (1981)CrossRefMATH

Bachmair, L., Dershowitz, N., Plaisted, D.: Completion without failure. In: Kaci, H.A., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures Progress in Theoretical Computer Science. Rewriting Techniques, vol. 2, pp. 1–30. Academic Press, New York (1989)

Ballantyne, A., Bledsoe, W.: On generating and using examples in proof discovery. In: Hayes, J., Michie, D., Pao, Y.H. (eds.) Machine Intelligence, vol. 10, pp. 3–39. Ellis Horwood, Chichester (1982)

Baumgartner, P., Thorstensen, E.: Instance based methods - a brief overview. Ger. J. Artif. Intell. (KI) 24(1), 35–42 (2010)

Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4–5), 591–632 (2008)MathSciNetCrossRefMATH

Bibel, W.: Automated Theorem Proving. Vieweg, Braunschweig (1982)CrossRefMATH

Billon, J.P.: The disconnection method. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol. 1071, pp. 110–126. Springer, Heidelberg (1996) CrossRef

Bledsoe, W.W.: Non-resolution theorem proving. Artif. Intell. 9(1), 1–35 (1977)MathSciNetCrossRefMATH

Bledsoe, W.W.: Using examples to generate instantiations of set variables. In: Proceedings of the 8th International Joint Conference on Artificial Intelligence, pp. 892–901. William Kaufmann (1983)

10.

Bledsoe, W.W., Loveland, D.W. (eds.): Automated Theorem Proving: After 25 Years. Contemporary mathematics. American Mathematical Society, Providence (1984) MATH

11.

Bonacina, M.P., Furbach, U., Sofronie-Stokkermans, V.: On first-order model-based reasoning. In: Martí-Oliet, N., Olveczky, P., Talcott, C. (eds.) Logic, Rewriting, and Concurrency: Essays in Honor of José Meseguer. LNCS, vol. 9200, Springer, Heidelberg (2015, to appear)

12.

Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Konev, B., Moura, L.D., Schulz, S. (eds.) Proceedings of the 4th Workshop on Practical Aspects in Automated Reasoning, EasyChair Proceedings in Computing (2014, to appear)

13.

Chang, C., Lee, R.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York (1973)MATH

14.

Chu, H., Plaisted, D.: Semantically guided first-order theorem proving using hyper-linking. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 192–206. Springer, Heidelberg (1994) CrossRef

15.

Claessen, K.: Equinox, a new theorem prover for full first-order logic with equality (2005). Presented at Dagstuhl Seminar on Deduction and Applications

16.

Davis, M.: Eliminating the irrelevant from machanical proofs. In: Proceedings of Symposia in Applied Mathematics, vol. 15, pp. 15–30 (1963)

17.

Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5, 394–397 (1962)MathSciNetCrossRefMATH

18.

Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201–215 (1960)MathSciNetCrossRefMATH

19.

Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279–301 (1982)MathSciNetCrossRefMATH

20.

Dubois, O.: Upper bounds on the satisfiability threshold. Theor. Comput. Sci. 265(1–2), 187–197 (2001)CrossRefMATH

21.

Feigenbaum, E.A., Feldman, J.: Computers and Thought. McGraw-Hill, New York (1963)MATH

22.

Gaillourdet, J.-M., Hillenbrand, T., Löchner, B., Spies, H.: The new WALDMEISTER loop at work. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 317–321. Springer, Heidelberg (2003) CrossRef

23.

Gelernter, H., Hansen, J., Loveland, D.: Empirical explorations of the geometry theorem proving machine. In: Feigenbaum, E., Feldman, J. (eds.) Computers and Thought, pp. 153–167. McGraw-Hill, New York (1963)

24.

Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006) CrossRef

25.

Gilmore, P.C.: A proof method for quantification theory. IBM J. Res. Dev. 4(1), 28–35 (1960)MathSciNetCrossRefMATH

26.

Green, C.: Application of theorem proving to problem solving. In: Proceedings of the 1st International Joint Conference on Artificial Intelligence, pp. 219–239. Morgan Kaufmann (1969)

27.

Greenbaum, S., Nagasaka, A., O’Rorke, P., Plaisted, D.A.: Comparison of natural deduction and locking resolution implementations. In: Loveland, D. (ed.) 6th Conference on Automated Deduction. LNCS, vol. 138, pp. 159–171. Springer, Heidelberg (1982) CrossRef

28.

Huet, G., Oppen, D.C.: Equations and rewrite rules: a survey. In: Book, R. (ed.) Formal Language Theory: Perspectives and Open Problems, pp. 349–405. Academic Press, New York (1980)

29.

Iturriaga, R.: Contributions to mechanical mathematics. Ph.D. thesis, Carnegie-Mellon University, Pittsburgh, Pennsylvania (1967)

30.

Jefferson, S., Plaisted, D.: Implementation of an improved relevance criterion. In: Proceedings of the 1st Conference on Artificial Intelligence Applications, pp. 476–482. IEEE Computer Society Press (1984)

31.

Joyner, W.: Resolution strategies as decision procedures. J. ACM 23(1), 398–417 (1976)MathSciNetCrossRefMATH

32.

Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)

33.

Korovin, K., Sticksel, C.: iProver-eq: an instantiation-based theorem prover with equality. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 196–202. Springer, Heidelberg (2010) CrossRef

34.

Lankford, D.: Canonical algebraic simplification in computational logic. Technical report, Memo ATP-25, University of Texas, Austin, Texas (1975)

35.

Lee, S.J., Plaisted, D.: Eliminating duplication with the hyper-linking strategy. J. Autom. Reasoning 9(1), 25–42 (1992)MathSciNetCrossRefMATH

36.

Loveland, D.: A simplified format for the model elimination procedure. J. ACM 16, 349–363 (1969)MathSciNetCrossRefMATH

37.

Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in prolog. In: Lusk, E., Overbeek, R. (eds.) 9th International Conference on Automated Deduction. LNCS, vol. 310, pp. 415–434. Springer, Heidelberg (1988) CrossRef

38.

McCune, W.W.: Otter 3.0 reference manual and guide. Technical report, ANL-94/6, Argonne National Laboratory, Argonne, IL (1994)

39.

Musser, D.: On proving inductive properties of abstract data types. In: Proceedings of the 7th ACM Symposium on Principles of Programming Languages, pp. 154–162. ACM Press (1980)

40.

O’Connor, J.J., Robertson, E.F.: Jacques Herbrand. http://www-history.mcs.st-andrews.ac.uk/Biographies/Herbrand.html. Accessed March 2015

41.

Otten, J.: PleanCoP 2.0 and ileanCoP 1.2: high performance lean theorem proving in classical and intuitionistic logic (system descriptions). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 283–291. Springer, Heidelberg (2008) CrossRef

42.

Paramasivam, M., Plaisted, D.: A replacement rule theorem prover. J. Autom. Reasoning 18(2), 221–226 (1997)CrossRef

43.

Pelletier, F.J.: Seventy-five problems for testing automatic theorem provers. J. Autom. Reasoning 2, 191–216 (1986)MathSciNetCrossRefMATH

44.

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)

45.

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)

46.

Plaisted, D.: An efficient relevance criterion for mechanical theorem proving. In: Proceedings of the 1st Annual National Conference on Artificial Intelligence, pp. 79–83. AAAI Press (1980)

47.

Plaisted, D.: A simplified problem reduction format. Artif. Intell. 18(2), 227–261 (1982)MathSciNetCrossRefMATH

48.

Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2, 293–304 (1986)MathSciNetCrossRefMATH

49.

Plaisted, D., Zhu, Y.: The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis. Vieweg, Wiesbaden (1997)CrossRefMATH

50.

Plaisted, D., Yahya, A.: A relevance restriction strategy for automated deduction. Artif. Intell. 144(1–2), 59–93 (2003)MathSciNetCrossRefMATH

51.

Plaisted, D.A.: Non-Horn clause logic programming without contrapositives. J. Autom. Reasoning 4(3), 287–325 (1988)MathSciNetCrossRefMATH

52.

Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reasoning 25(3), 167–217 (2000)MathSciNetCrossRefMATH

53.

Reif, W., Schellhorn, G.: Theorem proving in large theories. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction - A Basis for Applications. Applied Logic Series, vol. 10, pp. 225–241. Springer, Heidelberg (1998) CrossRef

54.

Riazanov, A., Voronkov, A.: Vampire. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 292–296. Springer, Heidelberg (1999) CrossRef

55.

Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)MATH

56.

Robinson, J.: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1(3), 227–234 (1965)MATH

57.

Robinson, J.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)CrossRefMATH

58.

Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013) CrossRef

59.

Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning 1: Classical Papers on Computational Logic 1957–1966. Symbolic Computation. Springer, Heidelberg (1983) MATH

60.

Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning 2: Classical Papers on Computational Logic 1967–1970. Symbolic Computation. Springer, Heidelberg (1983) MATH

61.

Letz, R., Stenz, G.: DCTP - a disconnection calculus theorem prover - system abstract. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 381–385. Springer, Heidelberg (2001) CrossRef

62.

Stickel, M.: A unification algorithm for associative-commutative functions. J. ACM 28(3), 423–434 (1981)MathSciNetCrossRefMATH

63.

Stickel, M.: A prolog technology theorem prover: implementation by an extended prolog compiler. J. Autom. Reasoning 4(4), 353–380 (1988)MathSciNetCrossRefMATH

64.

Sutcliffe, G.: The TPTP problem library and associated infrastructure - the FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337–362 (2009)CrossRefMATH

65.

Sutcliffe, G., Puzis, Y.: SRASS - a semantic relevance axiom selection system. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 295–310. Springer, Heidelberg (2007) CrossRef

66.

Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009) CrossRef

67.

Wikipedia: Hilbert’s program – Wikipedia, the free encyclopedia (2014). http://en.wikipedia.org/wiki/Hilbert’sprogram. Accessed March 2015

68.

Wos, L., Carson, D., Robinson, G.: The unit preference strategy in theorem proving. In: Proceedings of the Fall Joint Computer Conference, Part I. AFIPS Conference Proceedings, vol. 26, pp. 615–621 (1964)

69.

Zak, R.: Hilbert’s program. In: Zalta, E. (ed.) The Stanford Encyclopedia of Philosophy, Spring 2015 edn. (2015). Accessed March 2015

70.

Zalta, E.N.: Gottlob Frege. In: Zalta, E. (ed.) The Stanford Encyclopedia of Philosophy. Fall 2014 edn. (2014). Accessed March 2015

71.

Zamov, N.: Maslov’s inverse method and decidable classes. Ann. Pure Appl. Logic 42, 165–194 (1989)MathSciNetCrossRefMATH

Title: History and Prospects for First-Order Automated Deduction
Author: David A. Plaisted
Publisher: Springer International Publishing
Book: Automated Deduction - CADE-25
Print ISBN: 978-3-319-21400-9

Electronic ISBN: 978-3-319-21401-6

Copyright Year: 2015
DOI: https://doi.org/10.1007/978-3-319-21401-6_1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner