Efficient verified (UN)SAT certificate checking

DOI10.1007/978-3-319-63046-5_15MaRDI QIDQ5920089zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Efficient verified (UN)SAT certificate checking
• Efficient, verified checking of propositional proofs
• Producing and verifying extremely large propositional refutations
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• A unified framework for DPLL(T) + certificates

Cited in

(26)

• 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
• Certifying emptiness of timed Büchi automata
• A flexible proof format for SAT solver-elaborator communication
• Flexible proof production in an industrial-strength SMT solver
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• From LCF to Isabelle/HOL
• Formally verifying the solution to the Boolean Pythagorean triples problem
• A unified framework for DPLL(T) + certificates
• Efficient certified RAT verification
• Truth assignments as conditional autarkies
• Proofs and Certificates for Max-SAT
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• The resolution of Keller's conjecture
• Efficient verified (UN)SAT certificate checking
• The resolution of Keller's conjecture
• Certified verification for algebraic abstraction
• Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
• Producing and verifying extremely large propositional refutations
• AI Planning Languages Semantics
• Verified SAT-Based AI Planning
• Upper Bounding Diameters of State Spaces of Factored Transition Systems
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• Progress in certifying hardware model checking results

Describes a project that uses

Uses Software

• Isabelle/HOL

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

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