zbMATH — the first resource for mathematics

Efficient, verified checking of propositional proofs. (English) Zbl 06821857
Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-66106-3/pbk; 978-3-319-66107-0/ebook). Lecture Notes in Computer Science 10499, 269-284 (2017).
Summary: Satisfiability (SAT) solvers – and software in general – sometimes have serious bugs. We mitigate these effects by validating the results. Today’s SAT solvers emit proofs that can be checked with reasonable efficiency. However, these checkers are not trivial and can have bugs as well. We propose to check proofs using a formally verified program that adds little overhead to the overall process of proof validation. We have implemented a sequence of increasingly efficient, verified checkers using the ACL2 theorem proving system, and we discuss lessons from this effort. This work is already being used in industry and is slated for use in the next SAT competition.
For the entire collection see [Zbl 1369.68009].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI