Abstract
The paper traces the development of a family of high-performance proof systems out of formal first-order logical systems due to Kurt Schütte. In a first step Schütte’s basic classical system is compressed by eliminating its redundancy leading to syntactic characterizations of validity exclusively in terms of formula features including connections. In a second step connection calculi for various logics are developed on the basis of this characterization. Their implementations, leanCoP for classical clausal logic, nanoCoP for classical non-clausal logic, ileanCoP for intuitionistic logic, and MleanCoP for various modal logics, turn out to be among the best performing proof systems internationally. Schütte’s influences to Automated Deduction are pointed out by way of this exposition.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Peter B. Andrews. Theorem proving via general matings. Journal of the ACM, 28:193–214, 1981.
Roger Antonsen. The Method of Variable Splitting. PhD thesis, University of Oslo, 2008.
Roger Antonsen and Arild Waaler. Liberalized variable splitting. J. Automated Reasoning, 38:3–30, 2007.
Owen L. Astrachan and Donald W. Loveland. Meteors: High performance theorem provers using model elimination. In Robert S. Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe, Automated Reasoning Series, pages 31–60. Kluwer Academic Publishers, 1991.
Paul Benacerraf and Hilary Putnam, editors. Philosophy of Mathematics. Cambridge University Press, 1964. ISBN 0-521-29648-X.
Christoph Benzmüller, Jens Otten, and Thomas Raths. Implementing and evaluating provers for first-order modal logics. In L. De Raedt et al., editor, 20th European Conference on Artificial Intelligence (ECAI 2012), pages 163–168, Amsterdam, 2012. IOS Press.
Evert Willem Beth. Semantic entailment and formal derivability. Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, 18(13):309–342, 1955.
L. Wolfgang Bibel. Reflexionen vor Reflexen – Memoiren eines Forschers. Cuvillier Verlag, Göttingen, 2017.
Wolfgang Bibel. An approach to a systematic theorem proving procedure in first-order logic. Computing, 12:43–55, 1974. First presented to the GI Annual Conference in 1971; also available as Bericht Nr. 7207, Technische Universität München, Abteilung Mathematik (1972).
Wolfgang Bibel. Syntax–directed, semantics–supported program synthesis. Artificial Intelligence, 14:243–261, 1980.
Wolfgang Bibel. On matrices with connections. Journal of ACM, 28:633–645, 1981. Also available as Bericht 79, Universität Karlsruhe, Institut für Angewandte Informatik und Formale Beschreibungsverfahren.
Wolfgang Bibel. Computationally improved versions of Herbrand’s theorem. In J. Stern, editor, Proceedings of the Herbrand Symposium, pages 11–28, Amsterdam, 1982. North–Holland.
Wolfgang Bibel. Matings in matrices. Comm. ACM, 26:844–852, 1983.
Wolfgang Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, second edition, 1987. First edition 1982.
Wolfgang Bibel. Research perspectives for logic and deduction. In Oliviero Stock and Marco Schaerf, editors, Reasoning, Action, and Interaction in AI Theories and Systems – Essays dedicated to Luigia Carlucci Aiello, volume 4155 of LNAI, pages 25–43. Springer, Berlin, 2006.
Wolfgang Bibel. Early history and perspectives of automated deduction. In J. Hertzberg, M. Beetz, and R. Englert, editors, Proceedings of the 30th Annual German Conference on Artificial Intelligence (KI-2007), volume 4667 of LNAI, pages 2–18, Berlin, 2007. Springer.
Wolfgang Bibel. A vision for automated deduction rooted in the connection method. In R. Schmidt and C. Nalon, editors, The 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017), volume 10501 of LNAI, pages 3–21. Springer, 2017.
Wolfgang Bibel, Stefan Brüning, Uwe Egly, and Thomas Rath. KoMeT. In A. Bundy, editor, Proceedings of the International Conference on Automated Deduction, CADE-94, Lecture Notes in Artificial Intelligence, pages 783–787, Berlin, 1994. Springer. 13 From Schütte’s Formal Systems to Modern Automated Deduction 249
Wolfgang Bibel and Elmar Eder. Methods and calculi for deduction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, chapter 3, pages 71–193. Oxford University Press, Oxford, 1993.
Wolfgang Bibel and Jens Otten. Experiments with connection method provers. Presented to the 4th Conference on Artificial Intelligence and Theorem Proving, AITP 2019, April 7-12, 2019, Obergurgl, Austria, 2019.
Wolfgang Bibel and J. Schreiber. Proof search in a Gentzen–like system of first–order logic. In E. Gelenbe and D. Poitier, editors, Proceedings of the International Computing Symposium, pages 205–212, Amsterdam, 1975. North–Holland.
George Boole. An Investigation of the Laws of Thought on Which are Founded the Mathematical Theories of Logic and Probabilities. Macmillan, 1854.
Martin Davis. The Prehistory and Early History of Automated Deduction. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning 1 – Classical Papers on Computational Logic 1957–1966, pages 1–28. Springer, Berlin, 1983.
Martin Davis. Engines of Logic – Mathematicians and the Origin of the Computer. Norton, New York, 2000.
Elmar Eder. The cut rule in theorem proving. In Steffen Hölldobler, editor, Intellectics and Computational Logic, volume 19 of Applied Logic Series, pages 101–123. Kluwer Academic Publishers, Dordrecht, 2000.
Jens Erik Fenstad and HaoWang. Thoralf Albert Skolem. In Dov M. Gabbay and John Woods, editors, Logic from Russell to Church, volume 5 of Handbook of the History of Logic, pages 127–194. Elsevier B.V., 2009.
Melvin C. Fitting. Proof methods for modal and intuitionistic logics. D. Reidel, Dordrecht, 1983.
Gottlob Frege. Begriffsschrift. Louis Nebert, Halle, 1879.
Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210 and 405–431, 1935. Engl. transl. in [66].
Alessio Guglielmi. Asystem of interaction and structure. ACM Transactions on Computational Logic, 8(1):1–64, January 2007.
Reiner Hähnle, Neil. V. Murray, and Erik Rosenthal. Linearity and regularity with negationnormal form. Theoretical Computer Science, 328:325–354, 2004.
Christian Mahesh Hansen. A Variable Splitting Theorem Prover. PhD thesis, University of Oslo, 2012.
David Hilbert and W. Ackermann. Grundzüge der Theoretischen Logik. Springer, 1928.
Kaarlo J. J. Hintikka. Form and content in quantification theory. Acta Philosophica Fennica, 8:7–55, 1955.
Stig Kanger. Provability in Logic. PhD thesis, University of Stockholm, 1957.
William Kneale and Martha Kneale. The Development of Logic. Clarendon Press, Oxford, 1984.
Reinhold Letz, Klaus Mayr, and Christoph Goller. Controlled integration of the cut rule into connection tableaux calculi. Journal of Automated Reasoning, 13:297–337, 1994.
Reinhold Letz, Johannes Schumann, Stephan Bayerl, and Wolfgang Bibel. SETHEO — A high-performance theorem prover for first-order logic. Journal of Automated Reasoning, 8(2):183–212, 1992.
Reinhold Letz and Gernot Stenz. Model elimination and connection tableau procedures. In Handbook of Automated Reasoning, pages 2015–2112. Elsevier Science Publishers, Amsterdam, 2001.
Doanld W. Loveland. Mechanical theorem proving by Model Elimination. Journal of the ACM, pages 236–251, 1968.
William McCune. Release of Prover9. In Mile high conference on quasi groups, loops and non associative systems, Denver, 2005.
Jens Otten. Clausal connection-based theorem proving in intuitionistic first-order logic. In TABLEAUX 2005, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 3702 of LNCS, pages 245–261, Berlin, 2005. Springer. 250 Wolfgang Bibel and Jens Otten
Jens Otten. leanCoP 2.0 and ileanCoP 1.2 – High performance lean theorem proving in classical and intuitionistic logic. In A. Armando, P. Baumgartner, and G. Dowek, editors, IJCAR 2008, volume 5195 of LNCS, pages 283–291, Heidelberg, 2008. Springer.
Jens Otten. Restricting backtracking in connection calculi. AI Communications, 23:159–182, 2010.
Jens Otten. A non-clausal connection calculus. In K. Brünnler and G. Metcalfe, editors, TABLEAUX 2011, volume 6793 of LNAI, pages 226–241, Heidelberg, 2011. Springer.
Jens Otten. Implementing connection calculi for first-order modal logics. In E. Ternovska, K. Korovin, and S. Schulz, editors, 9th International Workshop on the Implementation of Logics (IWIL 2012), Merida, Venezuela, 2012.
Jens Otten. MleanCoP: A connection prover for first-order modal logic. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, IJCAR 2014, volume 8562 of LNCS, pages 269–276, Heidelberg, 2014. Springer.
Jens Otten. nanoCoP: A non-clausal connection prover. In Nicola Olivetti and Ashish Tiwari, editors, IJCAR 2016, volume 9706 of LNCS, pages 302–312, Heidelberg, 2016. Springer.
Jens Otten. Non-clausal connection calculi for non-classical logics. In R. Schmidt and C. Nalon, editors, 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, LNAI 10501, pages 209–227, Cham, Switzerland, 2017. Springer.
Jens Otten. Proof search optimizations for non-clausal connection calculi. In B. Konev, J. Urban, and P. Rümmer, editors, Practical Aspects of Automated Reasoning, PAAR 2018,volume 2162 of CEUR Workshop Proceedings, pages 49–57. CEUR-WS.org, 2018.
Jens Otten and Wolfgang Bibel. leanCoP: Lean connection-based theorem proving. Journal of Symbolic Computation, 36:139–161, 2003.
Jens Otten and Wolfgang Bibel. Advances in connection-based automated theorem proving.In Jonathan Bowen, Mike Hinchey, and Ernst-Rüdiger Olderog, editors, Provably Correct Systems, NASA Monographs in Systems and Software Engineering, pages 211–241. Springer, London, 2017.
David A. Plaisted and Steven Greenbaum. A structure-preserving clause form translation. J. Symbolic Computation, 2(3):293–304, 1986.
Dag Prawitz. An improved proof procedure. Theoria, 26:102–139, 1960. Also contained in [63, 159–199].
Dag Prawitz, H. Prawitz, and Neri Voghera. A mechanical proof procedure and its realization in an electronic computer. J.ACM, 7:102–128, 1960.
Thomas Raths and Jens Otten. The QMLTP problem library for first-order modal logics. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, IJCAR 2012, volume 7364 of LNCS, pages 454–461. Springer, 2012.
Thomas Raths, Jens Otten, and Christoph Kreitz. The ILTP problem library for intuitionisticlogic. Journal of Automated Reasoning, 38:261–271, 2007.
John A. Robinson. A machine-oriented logic based on the resolution principle. Journal of ACM, 12:23–41, 1965.
John Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science Publishers, Amsterdam, 2001.
Kurt Schütte. Ein System des verknüpfenden Schließens. Archiv für Mathematische Logik und Grundlagen for schung, 2:55–67, 1956.
Kurt Schütte. Vollständige Systeme Modaler und Intuitionistischer Logik. Ergebnisse der Mathematik und ihrer Grenzgebiete, Band 42. Springer Verlag, Berlin, 1968.
Kurt Schütte. Proof Theory. Grundlehren der mathematischen Wissenschaften 225. Springer-Verlag, Berlin, 1977. English and revised version of: Beweistheorie (1960).
Jörg Siekmann and Graham Wrightson, editors. Automation of Reasoning —Classical Papers on Computational Logic 1957–1966, volume 1. Springer, Berlin, 1983.
Raymond M. Smullyan. First-Order Logic. Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-Verlag, Berlin, Heidelberg, New York, 1971.
Mark E. Stickel. A Prolog technology theorem prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, 4:353–380, 1988. 13 From Schütte’s Formal Systems to Modern Automated Deduction 251
M. E. Szabo, editor. The collected papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969.
Anne S. Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2nd edition, 2000.
Willard van Orman Quine. A proof procedure for quantification theory. J. Symbolic Logic,20:141–149, 1955.
Arild Waaler. Connections in nonclassical logics. In Handbook of Automated Reasoning, pages 1487–1578. Elsevier Science Publishers, Amsterdam, 2001. See [59].
Lincoln A. Wallen. Automated Deduction in Non-Classical Logics. MIT Press, Cambridge, Mass., 1990.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Bibel, W., Otten, J. (2020). From Schütte’s Formal Systems to Modern Automated Deduction. In: Kahle, R., Rathjen, M. (eds) The Legacy of Kurt Schütte. Springer, Cham. https://doi.org/10.1007/978-3-030-49424-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-49424-7_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-49423-0
Online ISBN: 978-3-030-49424-7
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)