Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2015 | OriginalPaper | Buchkapitel

History and Prospects for First-Order Automated Deduction

verfasst von : David A. Plaisted

Erschienen in: Automated Deduction - CADE-25

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Nächstes Kapitel Stumbling Around in the Dark: Lessons from Everyday Mathematics
Literatur
1.
2.
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)
3.
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)
4.
Baumgartner, P., Thorstensen, E.: Instance based methods - a brief overview. Ger. J. Artif. Intell. (KI) 24(1), 35–42 (2010)
5.
Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4–5), 591–632 (2008)MathSciNetCrossRefMATH
6.
7.
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
8.
9.
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.
18.
19.
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.
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.
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.
36.
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.
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.
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.
48.
49.
Plaisted, D., Zhu, Y.: The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis. Vieweg, Wiesbaden (1997)CrossRefMATH
50.
51.
52.
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.
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.
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.
Metadaten
Titel
History and Prospects for First-Order Automated Deduction
verfasst von
David A. Plaisted
Copyright-Jahr
2015
Buch
Automated Deduction - CADE-25

Print ISBN: 978-3-319-21400-9

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

Copyright-Jahr: 2015

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