Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A Vision for Automated Deduction Rooted in the Connection Method

  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10501))

Abstract

The paper presents an informal overview of the Connection Method in Automated Deduction. In particular, it points out its unique advantage over competing methods which consists in its formula-orientedness. Among the consequences of this unique feature are three striking advantages, viz. uniformity (over many logics), performance (due to its extreme compactness and goal-orientedness, evidenced by the leanCoP family of provers), and a global view over the proof process (enabling a higher-level guidance of the proof search). These aspects are discussed on the basis of the extensive work accumulated in the literature about this proof method. Along this line of research we envisage a bright future for the field and point out promising directions for future research.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Josef Urban was so kind to run the formula with several state-of-the-art provers. E processes still 1.2 million clauses which can be reduced to 36.1 thousand by automatically learned strategies (with BliStr [39]), while Prover9 succeeds already with 3.3 thousand clauses.

References

  1. Alemi, A.A., Chollet, F., Een, N., Irving, G., Szegedy, C., Urban, J.: Deepmath - Deep sequence models for premise selection. In: Lee, D., Sugiyama, M., Luxburg, U., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems 29 (NIPS 2016), pp. 2235–2243 (2016)

    Google Scholar 

  2. Andrews, P.B.: Refutations by matings. IEEE Trans. Comput. C–25, 193–214 (1976)

    MATH  MathSciNet  Google Scholar 

  3. Andrews, P.B.: Theorem proving via general matings. J. ACM 28, 193–214 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  4. Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, Orlando (1986)

    MATH  Google Scholar 

  5. Andrews, P.B.: On connections and higher-order logic. J. Autom. Reas. 5, 257–291 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  6. Andrews, P.B.: Classical type theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 965–1007. Elsevier Science, Amsterdam (2001). Chap. 15

    Chapter  Google Scholar 

  7. Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: a theorem proving system for classical type theory. J. Autom. Reas. 16, 321–353 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  8. Antonsen, R., Waaler, A.: Liberalized variable splitting. J. Autom. Reas. 38, 3–30 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  9. Beringer, A., Hölldobler, S., Kurfeß, F.: Spatial reasoning and connectionist inference. In: Bajcsy, R. (ed.) Proceedings of the International Joint Conference on Artificial Intelligence, IJCAI-95, pp. 1352–1357. IJCAII. Morgan Kaufmann, San Mateo (1995)

    Google Scholar 

  10. Bibel, L.W.: Reflexionen vor Reflexen - Memoiren eines Forschers. Cuvillier Verlag, Göttingen (2017)

    Google Scholar 

  11. Bibel, W.: 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)

    Article  MATH  MathSciNet  Google Scholar 

  12. Bibel, W.: Programmieren in der Sprache der Prädikatenlogik. (Rejected) thesis for “Habilitation” presented to the Faculty of Mathematics. Technische Universität München, January 1975

    Google Scholar 

  13. Bibel, W.: Advanced topics in automated deduction. In: Nossum, R.T. (ed.) ACAI 1987. LNCS, vol. 345, pp. 41–59. Springer, Heidelberg (1988). doi:10.1007/3-540-50676-4_9

    Chapter  Google Scholar 

  14. Bibel, W.: Perspectives on automated deduction. In: Boyer, R.S. (ed.) Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 77–104. Kluwer Academic, Utrecht (1991)

    Chapter  Google Scholar 

  15. Bibel, W., Eder, E.: Methods and calculi for deduction. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 1, pp. 71–193. Oxford University Press, Oxford (1993). Chap. 3

    Google Scholar 

  16. Bibel, W., Hölldobler, S., Würtz, J.: Cycle unification. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 94–108. Springer, Heidelberg (1992). doi:10.1007/3-540-55602-8_158

    Google Scholar 

  17. Bibel, W., Schmitt, P.H. (eds.): Automated Deduction - A Basis for Applications. Volume I: Foundations - Calculi and Methods. Applied Logic Series. Kluwer, Dordrecht (1998)

    MATH  Google Scholar 

  18. Bibel, W.: Matings in matrices. Comm. ACM 26, 844–852 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  19. Bibel, W.: Automated Theorem Proving, 2nd edn. Vieweg Verlag, Braunschweig (1987). First edition 1982

    Book  MATH  Google Scholar 

  20. Bibel, W.: Deduction: Automated Logic. Academic Press, London (1993)

    Google Scholar 

  21. Bibel, W.: Research perspectives for logic and deduction. In: Stock, O., Schaerf, M. (eds.) Reasoning, Action and Interaction in AI Theories and Systems. LNCS, vol. 4155, pp. 25–43. Springer, Heidelberg (2006). doi:10.1007/11829263_2

    Chapter  Google Scholar 

  22. Bibel, W.: Transition logic revisited. Logic J. IGPL (Interest Group Pure Appl. Logic) 16(4), 317–334 (2008)

    MATH  MathSciNet  Google Scholar 

  23. Bibel, W., Otten, J.: From Schütte’s formal systems to modern automated deduction. In: Kahle, R., Rathjen, M. (eds.) The Legacy of Kurt Schütte. Springer (2017, to appear)

    Google Scholar 

  24. Bishop, M.: A breadth-first strategy for mating search. CADE 1999. LNCS, vol. 1632, pp. 359–373. Springer, Heidelberg (1999). doi:10.1007/3-540-48660-7_32

    Chapter  Google Scholar 

  25. Brown, C.E.: Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church’s Type Theory. Studies in Logic: Logic and Cognitive Systems, vol. 10. College Publications, London (2007)

    MATH  Google Scholar 

  26. Eder, E.: Relative Complexities of First Order Calculi. Vieweg, Braunschweig (1992)

    Book  MATH  Google Scholar 

  27. Ertel, W., Schumann, J.M.P., Suttner, C.B.: Learning heuristics for a theorem prover using back propagation. In: Retti, J., Leidlmair, K. (eds.) 5. Österreichische Artificial-Intelligence-Tagung, vol. 208, pp. 87–95. Springer, Heidelberg (1989). doi:10.1007/978-3-642-74688-8_10

    Chapter  Google Scholar 

  28. Färber, M., Kaliszyk, C., Urban, J.: Monte carlo tableau proof search. In: de Moura, L. (ed.) Automated Deduction - CADE 26. CADE 2017. LNCS, vol. 10395, pp. 563–579. Springer, Cham (2017). doi:10.1007/978-3-319-63046-5_34

    Chapter  Google Scholar 

  29. Freitas, F., Otten, J.: A connection calculus for the description logic \( {\cal{ALC}} \). In: Khoury, R., Drummond, C. (eds.) AI 2016. LNCS, vol. 9673, pp. 243–256. Springer, Cham (2016). doi:10.1007/978-3-319-34111-8_30

    Google Scholar 

  30. Fronhöfer, B.: Memories of the tableaux workshop 1992. Personal communication, January 2017

    Google Scholar 

  31. Galmiche, D.: Connection methods in linear logic and proof nets construction. Theoret. Comput. Sci. 232, 231–272 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  32. Gentzen, G.: Untersuchungen über das logische Schließen. Math. Z. 39, 176–210 and 405–431 (1935). English transl. in [58]

    Google Scholar 

  33. Herbrand, J.J.: In: Goldfarb, W.D. (ed.) Logical Writings. Reidel, Dordrecht (1971)

    Google Scholar 

  34. Goller, C.: A Connectionist Approach for Learning Search-Control Heuristics for Automated Deduction Systems. Akademische Verlagsgesellschaft AKA, Berlin (1999)

    MATH  Google Scholar 

  35. Hähnle, R.: Early Tableaux, presented to the Conference TABLEAUX 2017 (2017)

    Google Scholar 

  36. Hansen, C.M.: A Variable Splitting Theorem Prover. Ph.D. thesis. University of Oslo (2012)

    Google Scholar 

  37. Herbrand, J.: Recherches sur la théorie de la démonstration. Travaux Soc. Sciences et Lettres Varsovie, Cl. 3 (Mathem. Phys.) (1930). English transl. in [33]

    Google Scholar 

  38. Hölldobler, S. (ed.): Intellectics and Computational Logic - Papers in Honor of Wolfgang Bibel. Applied Logic Series. Kluwer Academic Publishers, Dordrecht (2000)

    MATH  Google Scholar 

  39. Jakubuv, J., Urban, J.: BliStrTune: hierarchical invention of theorem proving strategies. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 43–52. ACM (2017)

    Google Scholar 

  40. Kaliszyk, C., Urban, J.: FEMaLeCoP: fairly efficient machine learning connection prover. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 88–96. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48899-7_7

    Chapter  Google Scholar 

  41. Kaliszyk, C., Urban, J., Vyskočil, J.: Certified connection tableaux proofs for HOL light and TPTP. In: CPP 2015 Proceedings of the 2015 Conference on Certified Programs and Proofs, pp. 59–66. ACM (2015)

    Google Scholar 

  42. Kohlhase, M.: Automated Deduction - A Basis for Applications, Vol. I: Foundations - Calculi and Methods, Applied Logic Series. In: Higher-Order Automated Theorem Proving, vol. 8, pp. 431–462. Kluwer, Dordrecht (1998). Chap. 13

    Google Scholar 

  43. Krause, D., Nobre, E., Musicante, M.: Bibel’s matrix connection method in para consistent logic: general concepts and implementation. In: 21st International Conference of the Chilean Computer Science Society, SCCC 2001, pp. 161–167. IEEE (2001)

    Google Scholar 

  44. Kreitz, C., Otten, J.: Connection-based theorem proving in classical and non-classical logics. J. Univ. Comput. Sci. 5(3), 88–112 (1999)

    MATH  MathSciNet  Google Scholar 

  45. Kreitz, C., Otten, J., Schmitt, S., Pientka, B.: Matrix-based constructive theorem proving. In: Hölldobler, S. (ed.) Intellectics and Computational Logic. Applied Logic Series. Kluwer Academic Publishers, Dordrecht (2000). doi:10.1007/978-94-015-9383-0_12

    Google Scholar 

  46. Loos, S., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: Eiter, T., Sands, D. (eds.) LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 46, pp. 85–105, EasyChair (2017). https://easychair.org/publications/paper/340345

  47. Otten, J.: Clausal connection-based theorem proving in intuitionistic first-order logic. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 245–261. Springer, Heidelberg (2005). doi:10.1007/11554554_19

    Chapter  Google Scholar 

  48. Otten, J.: leanCoP 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, vol. 5195, pp. 283–291. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71070-7_23

    Chapter  Google Scholar 

  49. Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23, 159–182 (2010)

    MATH  MathSciNet  Google Scholar 

  50. Otten, J.: A non-clausal connection calculus. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol. 6793, pp. 226–241. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22119-4_18

    Chapter  Google Scholar 

  51. 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), Merida, Venezuela (2012)

    Google Scholar 

  52. Otten, J.: MleanCoP: a connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 269–276. Springer, Cham (2014). doi:10.1007/978-3-319-08587-6_20

    Google Scholar 

  53. Otten, J.: nanoCoP: a non-clausal connection prover. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 302–312. Springer, Cham (2016). doi:10.1007/978-3-319-40229-1_21

    Google Scholar 

  54. Otten, J.: Non-clausal connection calculi for non-classical logics. In: Schmidt, R., Nalon, C. (eds.) TABLEAUX 2017. LNAI, vol. 10501, pp. 209–227. Springer, Cham (2017)

    Google Scholar 

  55. Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36, 139–161 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  56. Otten, J., Bibel, W.: Advances in connection-based automated theorem proving. In: Bowen, J., Hinchey, M., Olderog, E.R. (eds.) Provably Correct Systems, pp. 211–241. Springer, London (2016). doi:10.1007/978-3-319-48628-4_9

    Google Scholar 

  57. Smith, R.G., Eckroth, J.: Building AI applications: yesterday, today, and tomorow. AImagazine 38(1), 6–22 (2017)

    Article  Google Scholar 

  58. Szabo, M.E. (ed.): The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam (1969)

    MATH  Google Scholar 

  59. Urban, J., Vyskočil, J.: Theorem proving in large formal mathematics as an emerging AI field. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 240–257. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36675-8_13

    Chapter  Google Scholar 

Download references

Acknowledgement

I greatly appreciate a very careful reading and many suggestions by Peter Andrews, Cezary Kaliszyk, Jens Otten and Renate Schmidt as well as helpful comments and generous information on system run-times by Josef Urban. David Plaisted independently suggested in a private communication the use of deep learning techniques in AD.

Author information

Authors and Affiliations

  1. Darmstadt University of Technology, Darmstadt, Germany

    Wolfgang Bibel

Authors
  1. Wolfgang Bibel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wolfgang Bibel .

Editor information

Editors and Affiliations

  1. University of Manchester, Manchester, United Kingdom

    Renate A. Schmidt

  2. University of Brasília, Brasília D.F., Brazil

    Cláudia Nalon

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Bibel, W. (2017). A Vision for Automated Deduction Rooted in the Connection Method. In: Schmidt, R., Nalon, C. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2017. Lecture Notes in Computer Science(), vol 10501. Springer, Cham. https://doi.org/10.1007/978-3-319-66902-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66902-1_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66901-4

  • Online ISBN: 978-3-319-66902-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation