More Web Proxy on the site http://driver.im/

research-article

Open access

Certified Connection Tableaux Proofs for HOL Light and TPTP

Authors:

Cezary Kaliszyk,

Jiři VyskočilAuthors Info & Claims

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

Pages 59 - 66

https://doi.org/10.1145/2676724.2693176

Published: 13 January 2015 Publication History

Abstract

In recent years, the Metis prover based on ordered paramodulation and model elimination has replaced the earlier built-in methods for general-purpose proof automation in HOL4 and Isabelle/HOL. In the annual CASC competition, the leanCoP system based on connection tableaux has however performed better than Metis. In this paper we show how the leanCoP's core algorithm can be implemented inside HOL Light. leanCoP's flagship feature, namely its minimalistic core, results in a very simple proof system. This plays a crucial role in extending the MESON proof reconstruction mechanism to connection tableaux proofs, providing an implementation of leanCoP that certifies its proofs. We discuss the differences between our direct implementation using an explicit Prolog stack,to the continuation passing implementation of MESON present in HOL Light and compare their performance on all core HOL Light goals. The resulting prover can be also used as a general purpose TPTP prover. We compare its performance against the resolution based Metis on TPTP and other interesting datasets.

References

[1]

J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning, 52 (2): 191--213, 2014. ISSN 0168-7433. 10.1007/s10817-013-9286-5.

Digital Library

[2]

B. Beckert and J. Posegga. leanTAP: Lean tableau-based deduction. J. Autom. Reasoning, 15 (3): 339--358, 1995. 10.1007/BF00881804. URL http://dx.doi.org/10.1007/BF00881804.

[3]

S. Böhme and T. Nipkow. Sledgehammer: Judgement Day. In J. Giesl and R. Hähnle, editors, IJCAR, volume 6173 of LNCS, pages 107--121. Springer, 2010. ISBN 978-3-642-14202-4.

Digital Library

[4]

T. Gauthier and C. Kaliszyk. Premise selection and external provers for HOL4. In Certified Programs and Proofs (CPP'15), Lecture Notes in Computer Science. Springer, 2015. 10.1145/2676724.2693173. URL http://dx.doi.org/10.1145/2676724.2693173. http://dx.doi.org/10.1145/2676724.2693173.

Digital Library

[5]

J. Harrison. Optimizing Proof Search in Model Elimination. In M. McRobbie and J. Slaney, editors, Proceedings of the 13th International Conference on Automated Deduction, number 1104 in LNAI, pages 313--327. Springer, 1996.

Digital Library

[6]

J. Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009. ISBN 978-0-521-89957-4.

[7]

K. Hoder and A. Voronkov. Sine qua non for large theory reasoning. In N. Bjørner and V. Sofronie-Stokkermans, editors, CADE, volume 6803 of LNCS, pages 299--314. Springer, 2011. ISBN 978-3-642-22437-9.

Digital Library

[8]

J. Hurd. First-order proof tactics in higher-order logic theorem provers. In M. Archer, B. D. Vito, and C. Muñoz, editors, Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), number NASA/CP-2003-212448 in NASA Technical Reports, pages 56--68, Sept. 2003. URL http://techreports.larc.nasa.gov/ltrs/PDF/2003/cp/NASA-2003-cp212448.pdf.

[9]

C. Kaliszyk and J. Urban. Stronger automation for Flyspeck by feature weighting and strategy evolution. In J. C. Blanchette and J. Urban, editors, PxTP 2013, volume 14 of EPiC Series, pages 87--95. EasyChair, 2013.

[10]

C. Kaliszyk and J. Urban. MizAR 40 for Mizar 40. CoRR, abs/1310.2805, 2013.

[11]

C. Kaliszyk and J. Urban. PRocH: Proof reconstruction for HOL Light. In M. P. Bonacina, editor, CADE, volume 7898 of phLNCS, pages 267--274. Springer, 2013. ISBN 978-3-642-38573-5.

Digital Library

[12]

C. Kaliszyk and J. Urban. Learning-assisted theorem proving with millions of lemmas. J. Symbolic Computation, 2014. 10.1016/j.jsc.2014.09.032. http://dx.doi.org/10.1016/j.jsc.2014.09.032.

[13]

C. Kaliszyk and J. Urban. HOL(y)Hammer: Online ATP service for HOL Light. Mathematics in Computer Science, 2014. 10.1007/s11786-014-0182-0. http://dx.doi.org/10.1007/s11786-014-0182-0.

[14]

C. Kaliszyk and J. Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53 (2): 173--213, 2014. 10.1007/s10817-014-9303-3. URL http://dx.doi.org/10.1007/s10817-014-9303-3.

Digital Library

[15]

C. Kaliszyk, L. Mamane, and J. Urban. Machine learning of Coq proof guidance: First experiments. In T. Kutsia and A. Voronkov, editors, SCSS 2014, volume 30 of EPiC Series, pages 27--34. EasyChair, 2014.

[16]

L. Kovács and A. Voronkov. First-order theorem proving and Vampire. In N. Sharygina and H. Veith, editors, CAV, volume 8044 of LNCS, pages 1--35. Springer, 2013. ISBN 978-3-642-39798-1.

[17]

KuhlweinLTUH12D. Kühlwein, T. van Laarhoven, E. Tsivtsivadze, J. Urban, and T. Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In B. Gramlich, D. Miller, and U. Sattler, editors, IJCAR, volume 7364 of LNCS, pages 378--392. Springer, 2012. ISBN 978-3-642-31364-6.

Digital Library

[18]

D. Kühlwein, J. C. Blanchette, C. Kaliszyk, and J. Urban. MaSh: Machine learning for Sledgehammer. In S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors, ITP 2013, volume 7998 of LNCS, pages 35--50. Springer, 2013. 10.1007/978-3-642-39634-2_6. URL http://cl-informatik.uibk.ac.at/users/cek/docs/kuehlwein-itp13.pdf.

Digital Library

[19]

R. Letz and G. Stenz. Model elimination and connection tableau procedures. IncitetDBLP:books/el/RobinsonV01, pages 2015--2114. ISBN 0-444-50813-9.

[20]

D. W. Loveland. Mechanical theorem proving by model elimination. J. the ACM, 15 (2): 236--251, Apr. 1968.

Digital Library

[21]

W. McCune. Prover9 and Mace4. http://www.cs.unm.edu/ mccune/prover9/, 2005--2010.

[22]

W. McCune and L. Wos. Otter: The CADE-13 Competition Incarnations. J. Autom. Reasoning, 18 (2): 211--220, 1997.

Digital Library

[23]

A. Nonnengart and C. Weidenbach. Computing small clause normal forms. IncitetDBLP:books/el/RobinsonV01, pages 335--367. ISBN 0-444-50813-9.

[24]

J. Otten. Clausal connection-based theorem proving in intuitionistic first-order logic. In B. Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2005, Koblenz, Germany, September 14--17, 2005, Proceedings, volume 3702 of Lecture Notes in Computer Science, pages 245--261. Springer, 2005. ISBN 3-540-28931-3. 10.1007/11554554_19. URL http://dx.doi.org/10.1007/11554554_19.

Digital Library

[25]

J. Otten. Restricting backtracking in connection calculi. AI Commun., 23 (2-3): 159--182, 2010. 10.3233/AIC-2010-0464. URL http://dx.doi.org/10.3233/AIC-2010-0464.

[26]

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

Digital Library

[27]

L. C. Paulson. Automated reasoning and its applications. chapter Generic Automatic Proof Tools, pages 23--47. MIT Press, Cambridge, MA, USA, 1997. ISBN 0-262-22055-5.

Digital Library

[28]

L. C. Paulson. A generic tableau prover and its integration with Isabelle. J. UCS, 5 (3): 73--87, 1999.

[29]

L. C. Paulson and J. Blanchette. Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In 8th IWIL, 2010. Invited talk.

[30]

L. C. Paulson and K. W. Susanto. Source-level proof reconstruction for interactive theorem proving. In K. Schneider and J. Brandt, editors, TPHOLs, volume 4732 of LNCS, pages 232--245. Springer, 2007. ISBN 978-3-540-74590-7.

Digital Library

[31]

J. A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001. ISBN 0-444-50813-9.

Digital Library

[32]

S. Schulz. System description: E 1.8. In K. L. McMillan, A. Middeldorp, and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14--19, 2013. Proceedings, volume 8312 of Lecture Notes in Computer Science, pages 735--743. Springer, 2013. ISBN 978-3-642-45220-8. 10.1007/978-3-642-45221-5_49. URL http://dx.doi.org/10.1007/978-3-642-45221-5_49.

[33]

M. E. Stickel. A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler. J. Autom. Reasoning, 4 (4): 353--380, 1988. 10.1007/BF00297245. URL http://dx.doi.org/10.1007/BF00297245.

Digital Library

[34]

T. Ströder, F. Emmes, P. Schneider-Kamp, J. Giesl, and C. Fuhs. A linear operational semantics for termination and complexity analysis of ISO Prolog. In G. Vidal, editor, LOPSTR, volume 7225 of LNCS, pages 237--252, 2012. 10.1007/978-3-642-32211-2_16.

Digital Library

[35]

G. Sutcliffe. The CADE-21 automated theorem proving system competition. AI Commun., 21 (1): 71--81, 2008. URL http://iospress.metapress.com/content/q3717606w4338313/.

Digital Library

[36]

J. Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37 (1-2): 21--43, 2006.

Digital Library

[37]

J. Urban and J. Vyskočil. Theorem proving in large formal mathematics as an emerging AI field. In M. P. Bonacina and M. E. Stickel, editors, Automated Reasoning and Mathematics: Essays in Memory of William McCune, volume 7788 of LNAI, pages 240--257. Springer, 2013. 10.1007/978-3-642-36675-8_13.

Digital Library

[38]

J. Urban, K. Hoder, and A. Voronkov. Evaluation of automated theorem proving on the Mizar Mathematical Library. In ICMS, pages 155--166, 2010.

Digital Library

[39]

J. Urban, J. Vyskočil, and P. Štěpánek. MaLeCoP: Machine learning connection prover. In K. Brünnler and G. Metcalfe, editors, TABLEAUX, volume 6793 of LNCS, pages 263--277. Springer, 2011. ISBN 978-3-642-22118-7.

Digital Library

[40]

J. Urban, P. Rudnicki, and G. Sutcliffe. ATP and presentation service for Mizar formalizations. J. Autom. Reasoning, 50: 229--241, 2013. 10.1007/s10817-012-9269-y.

Digital Library

[41]

C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, E. Keen, C. Theobalt, and D. Topić. System description: SPASS version 1.0.0. In Automated Deduction - CADE-16, volume 1632 of LNCS, pages 378--382. Springer Berlin Heidelberg, 1999. ISBN 978-3-540-66222-8. 10.1007/3-540-48660-7_34. URL http://dx.doi.org/10.1007/3-540-48660-7_34.

Digital Library

Cited By

Abdelaziz ICrouse MMakni BAustel VCornelio CIkbal SKapanipathi PMakondo NSrinivas KWitbrock MFokoue A(2023)Learning to Guide a Saturation-Based Theorem ProverIEEE Transactions on Pattern Analysis and Machine Intelligence10.1109/TPAMI.2022.314038245:1(738-751)Online publication date: 1-Jan-2023
https://doi.org/10.1109/TPAMI.2022.3140382
Shminke B(2023)gym-saturation: Gymnasium Environments for Saturation Provers (System description)Automated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_11(187-199)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_11
Färber MPopescu AZdancewic S(2022)Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewritingProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503683(225-238)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503683
Show More Cited By

Index Terms

Certified Connection Tableaux Proofs for HOL Light and TPTP
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation
  1. Models of computation
    1. Computability
  2. Theory and algorithms for application domains
    1. Machine learning theory
      1. Inductive inference

Recommendations

Learning-Assisted Automated Reasoning with Flyspeck

The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the Flyspeck proofs, producing an AI system capable of proving a ...
Connection Tableaux with Lazy Paramodulation

It is well known that the connection refinement of clause tableaux with paramodulation is incomplete (even with weak connections). In this paper, we present a new connection tableau calculus for logic with equality. This calculus is based on a lazy form ...
Safety and conservativity of definitions in HOL and Isabelle/HOL

Definitions are traditionally considered to be a safe mechanism for introducing concepts on top of a logic known to be consistent. In contrast to arbitrary axioms, definitions should in principle be treatable as a form of abbreviation, and thus compiled ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

January 2015

192 pages

ISBN:9781450332965

DOI:10.1145/2676724

Program Chairs:
Xavier Leroy
Inria Paris-Rocquencourt, France
,
Alwen Tiu
Nanyang Technological University, Singapore

Copyright © 2015 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 January 2015

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Austrian Science Fund

Conference

POPL '15

Sponsor:

SIGPLAN

POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 13 - 14, 2015

Mumbai, India

Acceptance Rates

CPP '15 Paper Acceptance Rate 18 of 26 submissions, 69%;

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
426
Total Downloads

Downloads (Last 12 months)80
Downloads (Last 6 weeks)4

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Abdelaziz ICrouse MMakni BAustel VCornelio CIkbal SKapanipathi PMakondo NSrinivas KWitbrock MFokoue A(2023)Learning to Guide a Saturation-Based Theorem ProverIEEE Transactions on Pattern Analysis and Machine Intelligence10.1109/TPAMI.2022.314038245:1(738-751)Online publication date: 1-Jan-2023
https://doi.org/10.1109/TPAMI.2022.3140382
Shminke B(2023)gym-saturation: Gymnasium Environments for Saturation Provers (System description)Automated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_11(187-199)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_11
Färber MPopescu AZdancewic S(2022)Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewritingProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503683(225-238)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503683
Rawson MReger G(2021)Eliminating Models During Model EliminationAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-030-86059-2_15(250-265)Online publication date: 30-Aug-2021
https://doi.org/10.1007/978-3-030-86059-2_15
Zombori ZCsiszárik AMichalewski HKaliszyk CUrban J(2021)Towards Finding Longer ProofsAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-030-86059-2_10(167-186)Online publication date: 30-Aug-2021
https://doi.org/10.1007/978-3-030-86059-2_10
Färber MKaliszyk CUrban J(2020)Machine Learning Guidance for Connection TableauxJournal of Automated Reasoning10.1007/s10817-020-09576-7Online publication date: 5-Sep-2020
https://doi.org/10.1007/s10817-020-09576-7
Färber MKaliszyk C(2019)Certification of Nonclausal Connection Tableaux ProofsAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-030-29026-9_2(21-38)Online publication date: 14-Aug-2019
https://doi.org/10.1007/978-3-030-29026-9_2
Kaliszyk CUrban JMichalewski HOlšák M(2018)Reinforcement learning of theorem provingProceedings of the 32nd International Conference on Neural Information Processing Systems10.5555/3327546.3327559(8836-8847)Online publication date: 3-Dec-2018
https://dl.acm.org/doi/10.5555/3327546.3327559
Kunze F(2016)Towards the Integration of an Intuitionistic First-Order Prover into CoqElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.210.6210(30-35)Online publication date: 17-Jun-2016
https://doi.org/10.4204/EPTCS.210.6
Reis G(2015)Importing SMT and Connection proofs as expansion treesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.186.3186(3-10)Online publication date: 30-Jul-2015
https://doi.org/10.4204/EPTCS.186.3
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents