A unifying principle for clause elimination in first-order logic

DOI10.1007/978-3-319-63046-5_17zbMath1496.03048OpenAlexW2735126037MaRDI QIDQ2405255

Benjamin Kiesl, Martin Suda

Publication date: 22 September 2017

Full work available at URL: http://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3321

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Craig interpolation with clausal first-order tableaux ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ Truth Assignments as Conditional Autarkies ⋮ Set-blocked clause and extended set-blocked clause in first-order logic ⋮ SAT-Inspired Eliminations for Superposition