Document Open Access Logo

A Formally Verified Checker for First-Order Proofs

Author Seulkee Baek

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2021.6.pdf
  • Filesize: 0.64 MB
  • 13 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computing methodologies → Theorem proving algorithms
Keywords
  • TESC
  • TPTP
  • TSTP
  • ATP

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

The Verified TESC Verifier (VTV) is a formally verified checker for the new Theory-Extensible Sequent Calculus (TESC) proof format for first-order ATPs. VTV accepts a TPTP problem and a TESC proof as input, and uses the latter to verify the unsatisfiability of the former. VTV is written in Agda, and the soundness of its proof-checking kernel is verified in respect to a first-order semantics formalized in Agda. VTV shows robust performance in a comprehensive test using all eligible problems from the TPTP problem library, successfully verifying all but the largest 5 of 12296 proofs, with >97% of the proofs verified in less than 1 second.

Cite As Get BibTex

Seulkee Baek. A Formally Verified Checker for First-Order Proofs. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 6:1-6:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.6

Author Details

Seulkee Baek
  • Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This work has been partially supported by AFOSR grant FA9550-18-1-0120.

Acknowledgements

I'd like to thank Jeremy Avigad and the anonymous referees for their careful proofreading of drafts and advice for improvements.

Supplementary Materials

References

  1. Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A modular integration of sat/smt solvers to coq through proof witnesses. In International Conference on Certified Programs and Proofs, pages 135-150. Springer, 2011. Google Scholar
  2. Henk Barendregt and Freek Wiedijk. The challenge of computer mathematics. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 363(1835):2351-2375, 2005. Google Scholar
  3. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of agda-a functional language with dependent types. In International Conference on Theorem Proving in Higher Order Logics, pages 73-78. Springer, 2009. Google Scholar
  4. Mario Carneiro. Metamath zero: The cartesian theorem prover. arXiv preprint arXiv:1910.10703, 2019. Google Scholar
  5. Zakaria Chihani, Tomer Libal, and Giselle Reis. The proof certifier checkers. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 201-210. Springer, 2015. Google Scholar
  6. Luís Cruz-Filipe, Marijn JH Heule, Warren A Hunt, Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified rat verification. In International Conference on Automated Deduction, pages 220-236. Springer, 2017. Google Scholar
  7. Luís Cruz-Filipe, Joao Marques-Silva, and Peter Schneider-Kamp. Efficient certified resolution proof checking. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 118-135. Springer, 2017. Google Scholar
  8. Jared Davis and Magnus O Myreen. The reflective milawa theorem prover is sound (down to the machine code that runs it). Journal of Automated Reasoning, 55(2):117-183, 2015. Google Scholar
  9. Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In Indagationes Mathematicae (Proceedings), volume 75, pages 381-392. North-Holland, 1972. Google Scholar
  10. Kurt Gödel. Über formal unentscheidbare sätze der principia mathematica und verwandter systeme i. Monatshefte für mathematik und physik, 38(1):173-198, 1931. Google Scholar
  11. John Harrison. Towards self-verification of hol light. In International Joint Conference on Automated Reasoning, pages 177-191. Springer, 2006. Google Scholar
  12. Marijn Heule, Warren Hunt, Matt Kaufmann, and Nathan Wetzler. Efficient, verified checking of propositional proofs. In International Conference on Interactive Theorem Proving, pages 269-284. Springer, 2017. Google Scholar
  13. Marijn JH Heule, Warren A Hunt, and Nathan Wetzler. Verifying refutations with extended resolution. In International Conference on Automated Deduction, pages 345-359. Springer, 2013. Google Scholar
  14. Marijn JH Heule, Warren A Hunt Jr, and Nathan Wetzler. Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Software Testing, Verification and Reliability, 24(8):593-607, 2014. Google Scholar
  15. Ramana Kumar, Rob Arthan, Magnus O Myreen, and Scott Owens. Hol with definitions: Semantics, soundness, and a verified implementation. In International Conference on Interactive Theorem Proving, pages 308-324. Springer, 2014. Google Scholar
  16. William McCune and Olga Shumsky. Ivy: A preprocessor and proof checker for first-order logic. In Computer-Aided reasoning, pages 265-281. Springer, 2000. Google Scholar
  17. Giles Reger and Martin Suda. Checkable proofs for first-order theorem proving. In ARCADE@ CADE, pages 55-63, 2017. Google Scholar
  18. Giles Reger, Martin Suda, and Andrei Voronkov. Testing a saturation-based theorem prover: Experiences and challenges. In International Conference on Tests and Proofs, pages 152-161. Springer, 2017. Google Scholar
  19. Alexandre Riazanov and Andrei Voronkov. The design and implementation of vampire. AI communications, 15(2, 3):91-110, 2002. Google Scholar
  20. Stephan Schulz. E-a brainiac theorem prover. Ai Communications, 15(2, 3):111-126, 2002. Google Scholar
  21. Raymond M Smullyan. First-order logic. Courier Corporation, 1995. Google Scholar
  22. Geoff Sutcliffe. Semantic derivation verification: Techniques and implementation. International Journal on Artificial Intelligence Tools, 15(06):1053-1070, 2006. Google Scholar
  23. Geoff Sutcliffe. The TPTP problem library and associated infrastructure. Journal of Automated Reasoning, 43(4):337, 2009. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact