Testing a saturation-based theorem prover: experiences and challenges

DOI10.1007/978-3-319-61467-0_10MaRDI QIDQ5086225zbMATH OpenOpenAlexFDO

Authors Giles Reger, Martin Suda, Andrei Voronkov

Publication date 1 July 2022

Published in Tests and Proofs (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1704.03391, https://www.research.manchester.ac.uk/portal/en/publications/testing-a-saturationbased-theorem-prover-experiences-and-challenges(f70b88cf-6bdc-4877-983e-b80de347167a).html

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience developing the theorem prover Vampire. We describe the techniques we currently employ to ensure that Vampire is correct and use this to motivate future challenges that need to be addressed to make this process more straightforward and to achieve better correctness guarantees.

Recommendations

• scientific article; zbMATH DE number 1746646
• Efficiently checking propositional refutations in HOL theorem provers
• A comprehensive framework for saturation theorem proving
• Integrating a SAT solver with an LCF-style theorem prover
• A comprehensive framework for saturation theorem proving

Cited in

(2)

• How to avoid the formal verification of a theorem prover
• Building Theorem Provers

Describes a project that uses

Uses Software

• VAMPIRE

This page was built for publication: Testing a saturation-based theorem prover: experiences and challenges

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5086225)