Document Open Access Logo

A Formally Verified Checker for First-Order Proofs

Author Seulkee Baek

PDF
Thumbnail PDF

File

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

Document Identifiers

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.

Cite AsGet 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

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.

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

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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact