Strong extension-free proof systems

DOI10.1007/s10817-019-09516-0zbMath1468.03011OpenAlexW2918119152WikidataQ90744223 ScholiaQ90744223MaRDI QIDQ2303251

Benjamin Kiesl, Armin Biere, Marijn J. H. Heule

Publication date: 3 March 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-019-09516-0

zbMATH Keywords

propositional proof systemsproof complexitySATextended resolutionproof checkingpigeonhole problemclause redundancy

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (8)

Unnamed Item ⋮ Simulating strong practical proof systems with extended resolution ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Preprocessing of propagation redundant clauses ⋮ Non-clausal redundancy properties ⋮ Covered clauses are not propagation redundant ⋮ Clause redundancy and preprocessing in maximum satisfiability ⋮ Preprocessing of propagation redundant clauses

Uses Software

• DRAT-trim

Cites Work

• Unnamed Item
• Unnamed Item
• Simulating circuit-level simplifications on CNF
• Producing and verifying extremely large propositional refutations
• Computer-aided proof of Erdős discrepancy properties
• Efficient SAT-based bounded model checking for software verification
• A simplified way of proving trade-off results for resolution
• The intractability of resolution
• Solving satisfiability in less than \(2^ n\) steps
• Extended resolution simulates \({\mathsf{DRAT}}\)
• On a generalization of extended resolution
• What a difference a variable makes
• Short proofs without new variables
• Super-Blocked Clauses
• Improved Static Symmetry Breaking for SAT
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Inprocessing Rules
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Expressing Symmetry Breaking in DRAT Proofs
• The Complexity of Propositional Proofs
• Bounded model checking using satisfiability solving

This page was built for publication: Strong extension-free proof systems