Advertisement

Advances in Connection-Based Automated Theorem Proving

  • Jens Otten
  • Wolfgang BibelEmail author
Chapter
Part of the NASA Monographs in Systems and Software Engineering book series (NASA)

Abstract

Automatic reasoning tools play an important role when developing provably correct software. Both main approaches, program verification and program synthesis employ automated reasoning tools, more specifically, automated theorem provers. Besides classical logic, non-classical logics are particularly relevant in this field. This chapter presents calculi to automate theorem proving in classical and some important non-classical logics, namely first-order intuitionistic and first-order modal logics. These calculi are based on the connection method, which permits a goal-oriented and, hence, a more efficient proof search. The connection calculi for these non-classical logics extend the calculus for classical logic in an elegant and uniform way by adding so-called prefixes to atomic formulae. The leanCoP theorem prover is a very compact PROLOG implementation of the connection calculus for classical logics. We present details of the implementation and describe some basic techniques to improve its efficiency. leanCoP is adapted to non-classical logics by integrating a prefix unification algorithm, which depends on the specific logic. This results in leading theorem provers for the aforementioned non-classical logics.

Keywords

Modal Logic Classical Logic Intuitionistic Logic Sequent Calculus Automate Theorem Prove 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgements

We would like to thank several anonymous referees for their constructive comments which were helpful to improve the text. Our thanks are also due to the editors Jonathan Bowen, Michael Hinchey and Ernst-Ruediger Olderog for the organization of the ProCoS Workshop in 2015, for compiling this volume and for inviting us to both projects.

References

  1. 1.
  2. 2.
  3. 3.
  4. 4.
    Antonsen, R., Waaler, A.: Liberalized variable splitting. J. Autom. Reason. 38, 3–30 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Astrachan, O., Loveland, D.: METEORs: high performance theorem provers using model elimination. In: Bledsoe, W., Boyer, S. (eds.) Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 31–60. Kluwer, Amsterdam (1991)CrossRefGoogle Scholar
  6. 6.
    Andrews, P.B.: General matings. In: Joyner, W.H. (ed.) Fourth Workshop on Automated Deduction, pp. 19–25 (1979)Google Scholar
  7. 7.
    Andrews, P.B.: Theorem proving via general matings. J. ACM 28, 193–214 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Barwise, J.: An introduction to first-order logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 5–46. North-Holland, Amsterdam (1977)CrossRefGoogle Scholar
  9. 9.
    Blackburn, P., van Bentham, J., Wolter, F.: Handbook of Modal Logic. Elsevier, Amsterdam (2006)Google Scholar
  10. 10.
    Baumgartner, P., Eisinger, N., Furbach, U.: A confluent connection calculus. In: Hölldobler, S. (ed.) Intellectics and Computational Logic. Applied Logic Series 19, pp. 3–26. Kluwer, Dordrecht (2000)CrossRefGoogle Scholar
  11. 11.
    Bibel, W.: An approach to a systematic theorem proving procedure in first-order logic. Computing 12, 43–55 (1974)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Bibel, W.: Syntax-directed, semantics-supported program synthesis. Artificial Intelligence 14, 243–261 (1980)CrossRefGoogle Scholar
  13. 13.
    Bibel, W.: On matrices with connections. J. ACM 28, 633–645 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Bibel, W.: Matings in matrices. Commun. ACM 26, 844–852 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Bibel, W.: Automated Theorem Proving, 2nd edn. Vieweg, Braunschweig (1987)CrossRefzbMATHGoogle Scholar
  16. 16.
    Bibel, W.: Research perspectives for logic and deduction. In: Stock, O., Schaerf, M. (eds.) Reasoning. Action, and Interaction in AI Theories and Systems - Essays dedicated to Luigia Carlucci Aiello, LNAI 4155, pp. 25–43. Springer, Berlin (2006)Google Scholar
  17. 17.
    Bibel, W.: Early history and perspectives of automated deduction. In: Hertzberg, J., Beetz, M., Englert, R. (eds.) KI 2007. LNAI 4667, pp. 2–18. Springer, Berlin (2007)Google Scholar
  18. 18.
    Bibel, W., Brüning, S., Egly, U., Rath, T.: Open image in new window In: Bundy, A. (ed.) CADE-12. LNAI 814, pp. 783–787. Springer, Heidelberg (1994)Google Scholar
  19. 19.
    Bibel, W., Otten, J.: From schütte’s formal system to modern automated deduction. In: Kahle, R., Rathjen, M. (eds.), The Legacy of Kurt Schütte. Springer, London, to appearGoogle Scholar
  20. 20.
    Brandt, C., Otten, J., Kreitz, C., Bibel, W.: Specifying and verifying organizational security properties in first-order logic. In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis. LNAI 6463, pp. 38–53. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  21. 21.
    Benzmüller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: De Raedt, L., et al. (eds.) 20th European Conference on Artificial Intelligence (ECAI 2012), pp. 163–168. IOS Press, Amsterdam (2012)Google Scholar
  22. 22.
    Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing, pp. 151–158. ACM, New York (1971)Google Scholar
  23. 23.
    van Dalen, D.: Intuitionistic logic. In: Goble, L. (ed.) The Blackwell Guide to Philosophical Logic, pp. 224–257. Blackwell, Oxford (2001)Google Scholar
  24. 24.
    Deville, Y.: Logic Programming, Systematic Program Development. Addison-Wesley, Wokingham (1990)Google Scholar
  25. 25.
    Eder, E.: Relative Complexities of First Order Calculi. Vieweg, Braunschweig (1992)CrossRefzbMATHGoogle Scholar
  26. 26.
    Fisher, K.: HACMS: high assurance cyber military systems. In: Proceedings of the 2012 ACM Conference on High Integrity Language Technoloby, pp. 51–52. ACM, New York (2012)Google Scholar
  27. 27.
    Fitting, M.: Proof Methods for Modal and Intuitionistic Logic. D. Reidel, Dordrecht (1983)CrossRefzbMATHGoogle Scholar
  28. 28.
    Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)CrossRefzbMATHGoogle Scholar
  29. 29.
    Gentzen, G.: Untersuchungen über das logische Schließen. Math. Z. 39(176–210), 405–431 (1935)MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Goel, S., Hunt, W.A., Kaufmann, M.: Engineering a formal, executable x86 ISA simulator for software verification. In: Bowen, J.P., Hinchey, M., Olderog, E.-R. (eds.) Provably Correct Systems. Springer, London (2016)Google Scholar
  31. 31.
    Hähnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 100–178. Elsevier, Amsterdam (2001)Google Scholar
  32. 32.
    Hähnle, R., Murray, N.V., Rosenthal, E.: Linearity and regularity with negation normal form. Theor. Comput. Sci. 328, 325–354 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Hansen, C.: A Variable Splitting Theorem Prover. University of Oslo (2012)Google Scholar
  34. 34.
    Herbrand, J.J.: Recherches sur la théorie de la démonstration. Travaux Soc. Sciences et Lettres Varsovie, Cl. 3 Mathem. Phys. (1930)Google Scholar
  35. 35.
    Hoare, C.A.R.: The emperor’s old clothes. Commun. ACM 24, 75–83 (1981)CrossRefGoogle Scholar
  36. 36.
    Klein, G., Elphinstone, K., Heiser, G., Adronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: SeL4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM SIGOPS, pp. 207–220. ACM, New York (2009)Google Scholar
  37. 37.
    Lee, S.-J., Plaisted, D.: Eliminating duplicates with the hyper-linking strategy. J. Autom. Reason. 9, 25–42 (1992)CrossRefzbMATHGoogle Scholar
  38. 38.
    Letz, R., Stenz, G.: Model elimination and connection Tableau procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 2015–2114. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  39. 39.
    Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: a high-performance theorem prover. J. Autom. Reason. 8, 183–212 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  40. 40.
    Loveland, D.: Mechanical theorem proving by model elimination. J. ACM 15, 236–251 (1968)MathSciNetCrossRefzbMATHGoogle Scholar
  41. 41.
    McCune, W.: Release of Prover9. Mile High Conference on Quasigroups, Loops and Nonassociative Systems. Technical report, Denver (2005)Google Scholar
  42. 42.
    McLaughlin, S., Pfenning, F.: Efficient intuitionistic theorem proving with the polarized inverse method. In: Schmidt, R.A. (ed.) CADE-22. LNCS 5663, pp. 230–244. Springer, Heidelberg (2009)Google Scholar
  43. 43.
    Moore, J.S.: Computing verified machine address bounds during symbolic simulation of code. In: Bowen, J.P., Hinchey, M., Olderog, E.-R. (eds.) Provably Correct Systems. Springer, London (2016)Google Scholar
  44. 44.
    Otten, J.: Clausal connection-based theorem proving in intuitionistic first-order logic. In: Beckert, B. (ed.) TABLEAUX 2005. LNAI 3702, pp. 245–261. Springer, Heidelberg (2005)Google Scholar
  45. 45.
    Otten, J.: \({{ leanCoP}}\) 2.0 and \({{ ileanCoP}}\) 1.2: high performance lean theorem proving in classical and intuitionistic logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS 5195, pp. 283–291. Springer, Heidelberg (2008)Google Scholar
  46. 46.
    Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23, 159–182 (2010)MathSciNetzbMATHGoogle Scholar
  47. 47.
    Otten, J.: A Non-clausal Connection Calculus. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNAI 6793, pp. 226–241. Springer, Heidelberg (2011)Google Scholar
  48. 48.
    Otten, J.: Implementing connection calculi for first-order modal logics. In: Ternovska, E., Korovin, K., Schulz, S. (eds.), 9th International Workshop on the Implementation of Logics (IWIL 2012), EPiC, EasyChair, vol. 22, pp. 18–32 (2012)Google Scholar
  49. 49.
    Otten, J.: \({{ MleanCoP}}\): a connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNAI 8562, pp. 269–276. Springer, Heidelberg (2014)Google Scholar
  50. 50.
    Otten, J.: \({{ nanoCoP}}\): a non-clausal connection prover. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNAI 9706. Springer, Heidelberg (2016)Google Scholar
  51. 51.
    Otten, J., Bibel, W.: \({{ leanCoP}}\): lean connection-based theorem proving. J. Symb. Comput. 36, 139–161 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  52. 52.
    Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2, 293–304 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  53. 53.
    Prawitz, D.: A proof procedure with matrix reduction. In: Laudet, M., et al. (eds.) Symposium on Automatic Demonstration. Lecture Notes in Mathem, pp. 207–214. Springer, Berlin (1970)CrossRefGoogle Scholar
  54. 54.
    Rautenberg, W.: A Concise Introduction to Mathematical Logic. Springer, Heidelberg (2010)CrossRefzbMATHGoogle Scholar
  55. 55.
    Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic. J. Autom. Reason. 38, 261–271 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  56. 56.
    Raths, T., Otten, J.: The QMLTP problem library for first-order modal logics. In: Gramlich, B., et al. (eds.) IJCAR 2012. LNAI 7364, pp. 454–461. Springer, Heidelberg (2012)Google Scholar
  57. 57.
    Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12, 23–41 (1965)MathSciNetCrossRefzbMATHGoogle Scholar
  58. 58.
    Ray, S.: Scalable Techniques for Formal Verification. Springer, Heidelberg (2010)CrossRefzbMATHGoogle Scholar
  59. 59.
    Robinson, J.A.: Proof \(=\) guarantee \(+\) explanation. In: Hölldobler, S. (ed.) Intellectics and Computational Logic. Applied Logic Series 19, pp. 277–294. Kluwer, Dordrecht (2000)CrossRefGoogle Scholar
  60. 60.
    Robinson, J.A., Voronkov, A.: Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)zbMATHGoogle Scholar
  61. 61.
    Schulz, S.: E - a brainiac theorem prover. AI Commun. 15, 111–126 (2002)zbMATHGoogle Scholar
  62. 62.
    Smullyan, R.M.: First-Order Logic. Springer, Heidelberg (1968)CrossRefzbMATHGoogle Scholar
  63. 63.
    Statman, R.: Intuitionistic propositional logic is polynomial-space complete. Theoret. Comput. Sci. 9, 67–72 (1979)MathSciNetCrossRefzbMATHGoogle Scholar
  64. 64.
    Stickel, M.: A Prolog technology theorem prover: implementation by an extended Prolog compiler. J. Autom. Reason. 4, 353–380 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  65. 65.
    Sutcliffe, G.: The CADE-21 automated theorem proving system competition. AI Commun. 21, 71–81 (2008)MathSciNetzbMATHGoogle Scholar
  66. 66.
    Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43, 337–362 (2009)CrossRefzbMATHGoogle Scholar
  67. 67.
    Sutcliffe, G.: The CADE-22 automated theorem proving system competition - CASC-22. AI Commun. 23, 47–59 (2010)MathSciNetzbMATHGoogle Scholar
  68. 68.
    Sutcliffe, G.: The 5th IJCAR automated theorem proving system competition - CASC-J5. AI Commun. 24, 75–89 (2011)MathSciNetGoogle Scholar
  69. 69.
    Waaler, A.: Connections in nonclassical logics. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1487–1578. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  70. 70.
    Wallen, L.A.: Automated Deduction in Nonclassical Logics. MIT Press, Cambridge (1990)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.University of OsloOsloNorway
  2. 2.University of PotsdamPotsdamGermany
  3. 3.Darmstadt University of TechnologyDarmstadtGermany

Personalised recommendations