Compositional propositional proofs

DOI10.1007/978-3-662-48899-7_31MaRDI QIDQ3460074zbMATH OpenOpenAlexFDO

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

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)

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

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
• DRAT proofs for XOR reasoning
• Unsatisfiability proofs for distributed clause-sharing SAT solvers
• The merits of compositional abstraction: a case study in propositional logic

Describes a project that uses

Uses Software

• DRAT-trim
• PicoSAT
• MiniSat

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)