Compositional propositional proofs

DOI10.1007/978-3-662-48899-7_31zbMATH Open1471.68310OpenAlexW2294403058MaRDI QIDQ3460074FDOQ3460074

Authors: Marijn J. H. Heule, Armin Biere 

Publication date: 12 January 2016

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-48899-7_31

Recommendations

• PaSAT -- parallel SAT-checking with lemma exchange: Implementation and applications
• Efficient, verified checking of propositional proofs
• Producing and verifying extremely large propositional refutations
• Partitioning SAT instances for distributed solving
• Data compression for proof replay

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (9)

• Propositional proof skeletons
• Compilability of propositional abduction
• DRABT
• Recursive proof composition from accumulation schemes
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Condorcet's principle and the preference reversal paradox
• Unsatisfiability proofs for distributed clause-sharing SAT solvers
• DRAT proofs for XOR reasoning
• The merits of compositional abstraction: a case study in propositional logic

Uses Software

• MiniSat
• PicoSAT
• DRAT-trim

This page was built for publication: Compositional propositional proofs

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