Skip to main content
Registrieren
Springer Professional
SUCHE
MENÜ 1 2 3 4
nach oben

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Erschienen in: Journal of Automated Reasoning 4/2022

28.02.2022

Larry Wos: Visions of Automated Reasoning

verfasst von: Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2022

Einloggen, um Zugang zu erhalten
share
TEILEN

Abstract

This paper celebrates the scientific discoveries and the service to the automated reasoning community of Lawrence (Larry) T. Wos, who passed away in August 2020. The narrative covers Larry’s most long-lasting ideas about inference rules and search strategies for theorem proving, his work on applications of theorem proving, and a collection of personal memories and anecdotes that let readers appreciate Larry’s personality and enthusiasm for automated reasoning.
Vorheriger Artikel Six Decades of Automated Reasoning: Papers in Memory of Larry Wos
Nächster Artikel Set of Support, Demodulation, Paramodulation: A Historical Perspective

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 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 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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





Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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



 


Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren
Fußnoten
2
According to [16], the concept of UR resolution appeared independently in the NEU strategy [74], in the same year as [96].
 
Literatur
1.
2.
Armando, A., Bonacina, M., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(14), 1–15 (2009) MathSciNetMATHCrossRef
3.
Bachmair, L.: Canonical Equational Proofs. Birkhäuser (1991)
4.
Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. Assoc. Comput. Mach. 41(2), 236–276 (1994) MathSciNetMATHCrossRef
5.
Bachmair, L., Dershowitz, N., Plaisted, D.: Completion Without Failure. In: Ait-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures, pp. 1–30. Academic Press (1989)
6.
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994) MathSciNetMATHCrossRef
7.
Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction, A Basis for Applications I: Foundations—Calculi and Methods, no. 10 in Applied Logic Series, pp. 352–397. Kluwer Academic Publishers (1998)
8.
Beeson, M., Veroff, R., Wos, L.: Double-negation elimination in some propositional logics. Stud. Logica. 80(2–3), 195–234 (2005) MathSciNetMATHCrossRef
9.
Beeson, M., Wos, L.: OTTER proofs in Tarskian geometry. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proceedings of the 7th International Joint Conference on Automated Reasoning, no. 8562 in Lecture Notes in Computer Science, pp. 495–510 (2014)
10.
11.
Bentkamp, A., Blanchette, J., Cruanes, S., Waldmann, U.: Superposition for Lambda-free higher-order logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Proceedings of the 9th International Joint Conference on Automated Reasoning, no. 10900 in Lecture Notes in Computer Science, pp. 2–46 (2018)
12.
Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., Waldmann, U.: Superposition with Lambdas. In: Fontaine, P. (ed.) Proceedings of the 27th International Conference on Automated Deduction, no. 11716 in Lecture Notes in Computer Science, pp. 55–73. Springer (2019)
13.
Bhayat, A., Reger, G.: Set of Support for Higher-order Reasoning. In: Konev, B., Rümmer, P., Urban, J. (eds.) Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning, no. 2162 in CEUR Workshop Proceedings, pp. 2–16 (2018)
14.
Bhayat, A., Reger, G.: Restricted Combinatory Unification. In: Fontaine, P. (ed.) Proceedings of the 27th International Conference on Automated Deduction, no. 11716 in Lecture Notes in Computer Science, pp. 74–93. Springer-Verlag (2019)
15.
Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proceedings of the 10th International Joint Conference on Automated Reasoning, no. 12166 in Lecture Notes in Artificial Intelligence, pp. 278–296 (2020)
16.
Bibel, W.: Early history and perspectives of automated deduction. In: Hertzberg, J., Beetz, M., Englert, R. (eds.) Proceedings of the 30th German Annual Conference on Artificial Intelligence, no. 4667 in Lecture Notes in Computer Science, pp. 2–18. Springer (2007)
17.
Bonacina, M.P.: On the reconstruction of proofs in distributed theorem proving: a modified clause-diffusion method. J. Symb. Comput. 21(4–6), 507–522 (1996) MathSciNetMATHCrossRef
18.
Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Wooldridge, M., Veloso, M. (eds.) Artificial Intelligence Today, no. 1600 in Lecture Notes in Artificial Intelligence, pp. 43–84. Springer-Verlag (1999)
19.
Bonacina, M.P.: Parallel theorem proving. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 179–235. Springer (2018)
20.
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 Dedicated to José Meseguer, no. 9200 in Lecture Notes in Computer Science, pp. 181–204. Springer-Verlag (2015)
21.
Bonacina, M.P., Hsiang, J.: The clause-diffusion methodology for distributed deduction. Fund. Inform. 24(1–2), 177–207 (1995) MathSciNetMATH
22.
Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedure. Theoret. Comput. Sci. 146, 199–242 (1995) MathSciNetMATHCrossRef
23.
Bonacina, M.P., Lynch, C., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161–189 (2011) MathSciNetMATHCrossRef
24.
Bonacina, M.P., Plaisted, D.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reason. 56(2), 113–141 (2016) MathSciNetMATHCrossRef
25.
Bonacina, M.P., Plaisted, D.: Semantically-guided goal-sensitive reasoning: inference system and completeness. J. Autom. Reason. 59(2), 165–218 (2017) MathSciNetMATHCrossRef
26.
27.
Cruanes, S.: Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond. Ph.D. thesis, Ecole Polytechnique, Paris, France (2015)
28.
29.
Duarte, A., Korovin, K.: Implementing superposition in iProver. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proceedings of the 10th International Joint Conference on Automated Reasoning, no. 12167 in Lecture Notes in Artificial Intelligence, pp. 388–397 (2020)
30.
Ernst, Z., Fitelson, B., Harris, K., Wos, L.: Shortest axiomatizations of implicational \(S4\) and \(S5\). Notre Dame J. Formal Log. 43(3), 169–179 (2002) MathSciNetMATHCrossRef
31.
Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. J. Math. Comput. Sci. 6(4), 409–425 (2012) MathSciNetMATHCrossRef
32.
Fitelson, B., Wos, L.: Axiomatic proofs through automated reasoning. Bull. Sect. Log. 29(3), 125–136 (2000) MathSciNetMATH
33.
Ganzinger, H., de Nivelle, H.: A Superposition decision procedure for the guarded fragment with equality. In: Proceedings of the 14th Symposium on Logic in Computer Science, pp. 1043–6871. IEEE Computer Society (1999)
34.
Gleiss, B., Suda, M.: Layered clause selection for theory reasoning. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proceedings of the 10th International Joint Conference on Automated Reasoning, no. 12166 in Lecture Notes in Computer Science, pp. 402–409 (2020)
35.
Hillenbrand, T.: Citius altius fortius: lessons learned from the theorem prover Waldmeister. In: Dahn, I., Vigneron, L. (eds.) Proceedings of the 4th International Workshop on First-Order Theorem Proving, no. 86.1 in Electronic Notes in Theoretical Computer Science, pp. 1–13 (2003)
36.
Hsiang, J., Rusinowitch, M.: A new method for establishing refutational completeness in theorem proving. In: Siekmann, J.H. (ed.) Proceedings of the 8th International Conference on Automated Deduction, no. 230 in Lecture Notes in Computer Science, pp. 141–152. Springer-Verlag (1986)
37.
Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottman, T. (ed.) Proceedings of the 14th International Colloquium on Automata, Languages, and Programming, no. 267 in Lecture Notes in Computer Science, pp. 54–71. Springer-Verlag (1987)
38.
Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. J. Assoc. Comput. Machinery. 38(3), 559–587 (1991) MathSciNetMATHCrossRef
39.
Huet, G.: A complete proof of correctness of the Knuth–Bendix completion algorithm. J. Comput. Syst. Sci. 23(1), 11–21 (1981) MathSciNetMATHCrossRef
40.
Kinyon, M.: Proof simplification and automated theorem proving. Philos. Trans. R Soc. A 377(2140) (2019)
41.
Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: John, L. (ed.) Computational Problems in Abstract Algebras, pp. 263–297. Pergamon Press, Oxford (1970)
42.
Kovacs, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) Proceedings of the 25th International Conference on Computer Aided Verification, no. 8044 in Lecture Notes in Artificial Intelligence, pp. 1–35. Springer (2013)
43.
Lusk, E.: Controlling redundancy in large search spaces: argonne-style theorem proving through the years. In: Voronkov, A. (ed.) Proceedings of the 3rd International Conference on Logic Programming and Automated Reasoning, no. 624 in Lecture Notes in Artificial Intelligence, pp. 96–106. Springer (1992)
44.
Lusk, E., McCune, W., Overbeek, R.: ITP at Argonne national laboratory. In: Siekmann, J.H. (ed.) Proceedings of the 8th International Conference on Automated Deduction, no. 230 in Lecture Notes in Computer Science, pp. 697–698. Springer (1986)
45.
McCharen, J., Overbeek, R., Wos, L.: Problems and experiments for and with automated theorem-proving programs. IEEE Trans. Comput. C–25(8), 773–782 (1976) MATHCrossRef
46.
47.
McCune, W.: 33 Basic test problems: a practical evaluation of some paramodulation strategies. In: Veroff, R. (ed.) Automated Reasoning and its Applications: Essays in Honor of Larry Wos, pp. 71–114. MIT Press (1997)
48.
49.
McCune, W.: Otter 3.3 Reference Manual. Tech. Rep. ANL/MSC-TM-263, Argonne National Laboratory, Argonne, USA (2003)
50.
McCune, W., Veroff, R., Fitelson, B., Harris, K., Feist, A., Wos, L.: Short single axioms for Boolean algebra. J. Autom. Reason. 29(1), 1–16 (2002) MathSciNetMATHCrossRef
51.
McCune, W., Wos, L.: A case study in automated theorem proving: finding sages in combinatory logic. J. Autom. Reason. 3(1), 91–107 (1987) MathSciNetMATHCrossRef
52.
McCune, W., Wos, L.: Otter: the CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211–220 (1997) CrossRef
53.
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371–443. Elsevier Science (2001)
54.
55.
Parrello, B., Kabat, W., Wos, L.: Job-shop scheduling using automated reasoning: a case study of the car-sequencing problem. J. Autom. Reason. 2(1), 1–42 (1986) MathSciNetCrossRef
56.
Peterson, G.: A technique for establishing completeness results in theorem proving with equality. SIAM Journal of Computation 12(1), 82–100 (1983) MathSciNetMATHCrossRef
57.
Plaisted, D.: Equational reasoning and term rewriting systems. In: Gabbay, D., Hogger, C., Robinson, J. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 1, pp. 273–364. Oxford University Press (1993)
58.
Plaisted, D., Zhu, Y.: The Efficiency of Theorem Proving Strategies. Friedr. Vieweg & Sohn (1997)
59.
Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A., Middeldorp, A. (eds.) Proceedings of the 25th International Conference on Automated Deduction, no. 9195 in Lecture Notes in Computer Science, pp. 399–415. Springer-Verlag (2015)
60.
Robinson, G., Wos, L.: Paramodulation and theorem proving in first-order theories with equality. Mach. Intell. 4, 135–150 (1969) MathSciNetMATH
61.
62.
Robinson, J.: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227–234 (1965) MathSciNetMATH
63.
Rusinowitch, M.: Démonstration Automatique par des Techniques de Réécriture. Ph.D. thesis, Université de Nancy 1, Nancy, France (1987). Published in the series Collection Science Informatique, InterEdition, Paris, France (1989)
64.
65.
Schulz, S., Cruanes, S., Vukmirović, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) Proceedings of the 27th International Conference on Automated Deduction, no. 11716 in Lecture Notes in Computer Science, pp. 495–507. Springer (2019)
66.
Schulz, S., Möhrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Olivetti, N., Tiwari, A. (eds.) Proceedings of the 8th International Joint Conference on Automated Reasoning, no. 9706 in Lecture Notes in Artificial Intelligence, pp. 330–345 (2016)
67.
68.
Smith, B.: Reference manual for the environmental theorem prover: an incarnation of AURA. Tech. Rep. ANL/88-2, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, USA (1988)
69.
Smith, B., Wos, L.: An unnatural attack on the structure problem for the free Jordan ring on 3 letters: an application of quad arithmetic. In: Beck, R., Kolman, B. (eds.) Computers in nonassociative rings and algebras. Special Session of the 82nd Annual Meeting of the American Mathematical Society, pp. 45–138. Academic Press (1977)
70.
Smullyan, R.: To Mock a Mocking Bird and Other Logic Puzzles. Knopf (1978)
71.
Stickel, M.: PTTP and linked inference. In: R. Boyer (ed.) Automated Reasoning: Essays in Honor of Woody Bledsoe, Automated Reasoning Series, pp. 283–296. Kluwer Academic Publishers (1991)
72.
73.
74.
75.
Veroff, R.: Automated Reasoning and its Applications: Essays in Honor of Larry Wos. MIT Press (1997)
76.
77.
Vukmirović, P., Blanchette, J., Cruanes, S., Schulz, S.: Extending a brainiac prover to lambda-free higher-order logic. In: T. Vojnar, L. Zhang (eds.) Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, no. 11427 in Lecture Notes in Computer Science, pp. 192–210. Springer (2019)
78.
Vukmirović, P., Nummelin, V.: Boolean reasoning in a higher-order superposition prover. In: Fontaine, P., Rümmer, P., Tourret, S. (eds.) Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning, no. 2752 in CEUR Workshop Proceedings, pp. 148–166 (2020)
79.
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R. (ed.) Proceedings of the 22nd International Conference on Automated Deduction, no. 5663 in Lecture Notes in Artificial Intelligence, pp. 140–145. Springer (2009)
80.
Winker, S., Wos, L.: Automated generation of models and counterexamples and its application to open questions in ternary Boolean algebra. In: Proceedings of the 8th International Symposium on Multiple-Valued Logic, pp. 251–256. IEEE Press (1978)
81.
Winker, S., Wos, L., Lusk, E.: Semigroups, antiautomorphisms, and involutions: a computer solution to an open problem. Math. Comput. 37(156), 533–545 (1981) MathSciNetMATH
82.
Wos, L.: Automated Reasoning—33 Basic Research Problems. Prentice-Hall (1988)
83.
Wos, L.: The impossibility of the automation of logical reasoning. In: Kapur, D. (ed.) Proceedings of the 11th International Conference on Automated Deduction, no. 607 in Lecture Notes in Artificial Intelligence, pp. 1–3. Springer-Verlag (1992)
84.
85.
86.
87.
Wos, L.: The Automation of Reasoning: An Experimenter’s Notebook with OTTER Tutorial. Academic Press (1996)
88.
89.
Wos, L., Carson, D., Robinson, G.: The unit preference strategy in theorem proving. In: Proceedings of the AFIPS 1964 Fall Joint Computer Conference, pp. 615–621. Spartan Books (1964)
90.
Wos, L., Fitelson, B.: Automating the search for answers to open questions. In: Aagaard, M., Harrison, J. (eds.) Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, no. 1869 in Lecture Notes in Computer Science, pp. 519–525 (2000)
91.
Wos, L., Overbeek, R., Lusk, E.: Subsumption, a sometimes undervalued procedure. In: Lassez, J.L., Plotkin, G. (eds.) Computational Logic—Essays in Honor of Alan Robinson, pp. 3–40. MIT Press (1991)
92.
Wos, L., Pereira, F., Hong, R., Boyer, R., Moore, J., Bledsoe, W., Henschen, L., Buchanan, B., Wrightson, G., Green, C.: An overview of automated reasoning and related fields. J. Autom. Reason. 1(1), 5–48 (1985) MathSciNetMATHCrossRef
93.
Wos, L., Pieper, G.: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning. World Scientific (1999)
94.
Wos, L., Pieper, G.: Automated Reasoning and the Discovery of Missing and Elegant Proofs. Rinton Press (2003)
95.
Wos, L., Robinson, G., Carson, D.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12(4), 536–541 (1965) MathSciNetMATHCrossRef
96.
Wos, L., Robinson, G., Carson, D., Shalla, L.: The concept of demodulation in theorem proving. J. ACM 14(4), 698–709 (1967) MATHCrossRef
97.
98.
Wos, L., Ulrich, D., Fitelson, B.: Vanquishing the XCB question: the methodological discovery of the last shortest single Axiom for the equivalential calculus. J. Autom. Reason. 29(2), 107–124 (2002) MathSciNetMATHCrossRef
99.
Wos, L., Ulrich, D., Fitelson, B.: XCB, the last of the shortest single axioms for the classical equivalential calculus. Bull. Sect. Log. 32(3), 131–136 (2003) MathSciNetMATH
100.
Wos, L., Winker, S., Veroff, R., Smith, B., Henschen, L.: Questions concerning possible shortest single axioms in equivalential calculus: an application of automated theorem proving to infinite domains. Notre Dame J. Formnal Log. 24(2), 205–223 (1983) MATH
Metadaten
Titel
Larry Wos: Visions of Automated Reasoning
verfasst von
Michael Beeson
Maria Paola Bonacina
Michael Kinyon
Geoff Sutcliffe
Publikationsdatum
28.02.2022
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09620-8

Weitere Artikel der Ausgabe 4/2022

Journal of Automated Reasoning 4/2022 Zur Ausgabe

OriginalPaper

A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column

OriginalPaper

Fast Left Kan Extensions Using the Chase

OriginalPaper

Tuple Interpretations for Termination of Term Rewriting

OriginalPaper

A Formalization of the Smith Normal Form in Higher-Order Logic

OriginalPaper

A Formalization of Dedekind Domains and Class Groups of Global Fields

OriginalPaper

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory

Premium Partner