Short proofs without new variables
From MaRDI portal
Publication:2405245
DOI10.1007/978-3-319-63046-5_9zbMath1468.03010OpenAlexW2735859735MaRDI QIDQ2405245
Benjamin Kiesl, Armin Biere, Marijn J. H. Heule
Publication date: 22 September 2017
Full work available at URL: https://doi.org/10.1007/978-3-319-63046-5_9
Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Unnamed Item, Simulating strong practical proof systems with extended resolution, Truth Assignments as Conditional Autarkies, Preprocessing of propagation redundant clauses, Unnamed Item, The resolution of Keller's conjecture, Strong extension-free proof systems, Non-clausal redundancy properties, Covered clauses are not propagation redundant, The resolution of Keller's conjecture, Clause redundancy and preprocessing in maximum satisfiability, Preprocessing of propagation redundant clauses
