From Schütte’s Formal Systems to Modern Automated Deduction

1. Peter B. Andrews. Theorem proving via general matings. Journal of the ACM, 28:193–214, 1981.

   Google Scholar 

2. Roger Antonsen. The Method of Variable Splitting. PhD thesis, University of Oslo, 2008.

   Google Scholar 

3. Roger Antonsen and Arild Waaler. Liberalized variable splitting. J. Automated Reasoning, 38:3–30, 2007.

   Google Scholar 

4. 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.

   Google Scholar 

5. Paul Benacerraf and Hilary Putnam, editors. Philosophy of Mathematics. Cambridge University Press, 1964. ISBN 0-521-29648-X.

   Google Scholar 

6. 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.

   Google Scholar 

7. Evert Willem Beth. Semantic entailment and formal derivability. Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, 18(13):309–342, 1955.

   Google Scholar 

8. L. Wolfgang Bibel. Reflexionen vor Reflexen – Memoiren eines Forschers. Cuvillier Verlag, Göttingen, 2017.

   Google Scholar 

9. 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).

   Google Scholar 

10. Wolfgang Bibel. Syntax–directed, semantics–supported program synthesis. Artificial Intelligence, 14:243–261, 1980.

    Google Scholar 

11. 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.

    Google Scholar 

12. 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.

    Google Scholar 

13. Wolfgang Bibel. Matings in matrices. Comm. ACM, 26:844–852, 1983.

    Google Scholar 

14. Wolfgang Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, second edition, 1987. First edition 1982.

    Google Scholar 

15. 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.

    Google Scholar 

16. 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.

    Google Scholar 

17. 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.

    Google Scholar 

18. 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

    Google Scholar 

19. 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.

    Google Scholar 

20. 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.

    Google Scholar 

21. 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.

    Google Scholar 

22. George Boole. An Investigation of the Laws of Thought on Which are Founded the Mathematical Theories of Logic and Probabilities. Macmillan, 1854.

    Google Scholar 

23. 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.

    Google Scholar 

24. Martin Davis. Engines of Logic – Mathematicians and the Origin of the Computer. Norton, New York, 2000.

    Google Scholar 

25. 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.

    Google Scholar 

26. 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.

    Google Scholar 

27. Melvin C. Fitting. Proof methods for modal and intuitionistic logics. D. Reidel, Dordrecht, 1983.

    Google Scholar 

28. Gottlob Frege. Begriffsschrift. Louis Nebert, Halle, 1879.

    Google Scholar 

29. Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210 and 405–431, 1935. Engl. transl. in [66].

    Google Scholar 

30. Alessio Guglielmi. Asystem of interaction and structure. ACM Transactions on Computational Logic, 8(1):1–64, January 2007.

    Google Scholar 

31. Reiner Hähnle, Neil. V. Murray, and Erik Rosenthal. Linearity and regularity with negationnormal form. Theoretical Computer Science, 328:325–354, 2004.

    Google Scholar 

32. Christian Mahesh Hansen. A Variable Splitting Theorem Prover. PhD thesis, University of Oslo, 2012.

    Google Scholar 

33. David Hilbert and W. Ackermann. Grundzüge der Theoretischen Logik. Springer, 1928.

    Google Scholar 

34. Kaarlo J. J. Hintikka. Form and content in quantification theory. Acta Philosophica Fennica, 8:7–55, 1955.

    Google Scholar 

35. Stig Kanger. Provability in Logic. PhD thesis, University of Stockholm, 1957.

    Google Scholar 

36. William Kneale and Martha Kneale. The Development of Logic. Clarendon Press, Oxford, 1984.

    Google Scholar 

37. 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.

    Google Scholar 

38. 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.

    Google Scholar 

39. Reinhold Letz and Gernot Stenz. Model elimination and connection tableau procedures. In Handbook of Automated Reasoning, pages 2015–2112. Elsevier Science Publishers, Amsterdam, 2001.

    Google Scholar 

40. Doanld W. Loveland. Mechanical theorem proving by Model Elimination. Journal of the ACM, pages 236–251, 1968.

    Google Scholar 

41. William McCune. Release of Prover9. In Mile high conference on quasi groups, loops and non associative systems, Denver, 2005.

    Google Scholar 

42. 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

    Google Scholar 

43. 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.

    Google Scholar 

44. Jens Otten. Restricting backtracking in connection calculi. AI Communications, 23:159–182, 2010.

    Google Scholar 

45. 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.

    Google Scholar 

46. 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.

    Google Scholar 

47. 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.

    Google Scholar 

48. 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.

    Google Scholar 

49. 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.

    Google Scholar 

50. 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.

    Google Scholar 

51. Jens Otten and Wolfgang Bibel. leanCoP: Lean connection-based theorem proving. Journal of Symbolic Computation, 36:139–161, 2003.

    Google Scholar 

52. 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.

    Google Scholar 

53. David A. Plaisted and Steven Greenbaum. A structure-preserving clause form translation. J. Symbolic Computation, 2(3):293–304, 1986.

    Google Scholar 

54. Dag Prawitz. An improved proof procedure. Theoria, 26:102–139, 1960. Also contained in [63, 159–199].

    Google Scholar 

55. Dag Prawitz, H. Prawitz, and Neri Voghera. A mechanical proof procedure and its realization in an electronic computer. J.ACM, 7:102–128, 1960.

    Google Scholar 

56. 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.

    Google Scholar 

57. Thomas Raths, Jens Otten, and Christoph Kreitz. The ILTP problem library for intuitionisticlogic. Journal of Automated Reasoning, 38:261–271, 2007.

    Google Scholar 

58. John A. Robinson. A machine-oriented logic based on the resolution principle. Journal of ACM, 12:23–41, 1965.

    Google Scholar 

59. John Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science Publishers, Amsterdam, 2001.

    Google Scholar 

60. Kurt Schütte. Ein System des verknüpfenden Schließens. Archiv für Mathematische Logik und Grundlagen for schung, 2:55–67, 1956.

    Google Scholar 

61. Kurt Schütte. Vollständige Systeme Modaler und Intuitionistischer Logik. Ergebnisse der Mathematik und ihrer Grenzgebiete, Band 42. Springer Verlag, Berlin, 1968.

    Google Scholar 

62. Kurt Schütte. Proof Theory. Grundlehren der mathematischen Wissenschaften 225. Springer-Verlag, Berlin, 1977. English and revised version of: Beweistheorie (1960).

    Google Scholar 

63. Jörg Siekmann and Graham Wrightson, editors. Automation of Reasoning —Classical Papers on Computational Logic 1957–1966, volume 1. Springer, Berlin, 1983.

    Google Scholar 

64. Raymond M. Smullyan. First-Order Logic. Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-Verlag, Berlin, Heidelberg, New York, 1971.

    Google Scholar 

65. 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

    Google Scholar 

66. M. E. Szabo, editor. The collected papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969.

    Google Scholar 

67. Anne S. Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2nd edition, 2000.

    Google Scholar 

68. Willard van Orman Quine. A proof procedure for quantification theory. J. Symbolic Logic,20:141–149, 1955.

    Google Scholar 

69. Arild Waaler. Connections in nonclassical logics. In Handbook of Automated Reasoning, pages 1487–1578. Elsevier Science Publishers, Amsterdam, 2001. See [59].

    Google Scholar 

70. Lincoln A. Wallen. Automated Deduction in Non-Classical Logics. MIT Press, Cambridge, Mass., 1990.

    Google Scholar 

Download references