Efficient verified (UN)SAT certificate checking

DOI10.1007/978-3-319-63046-5_15zbMath1468.68133OpenAlexW2734612968MaRDI QIDQ5920089

Peter Lammich

Publication date: 22 September 2017

Published in: Automated Deduction – CADE 26 (Search for Journal in Brave)

Full work available at URL: https://www.research.manchester.ac.uk/portal/en/publications/efficient-verified-unsat-certificate-checking(751d0e95-6538-4012-a204-52d283d4abdc).html

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (15)

CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalization of the resolution calculus for first-order logic ⋮ Efficient, verified checking of propositional proofs ⋮ Unnamed Item ⋮ Truth Assignments as Conditional Autarkies ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points ⋮ Certifying emptiness of timed Büchi automata ⋮ From LCF to Isabelle/HOL ⋮ The resolution of Keller's conjecture ⋮ A flexible proof format for SAT solver-elaborator communication ⋮ Efficient verified (UN)SAT certificate checking ⋮ Formally verifying the solution to the Boolean Pythagorean triples problem ⋮ The resolution of Keller's conjecture ⋮ Flexible proof production in an industrial-strength SMT solver

Uses Software

• Isabelle/HOL

This page was built for publication: Efficient verified (UN)SAT certificate checking