Blocked Clauses in First-Order Logic

DOI10.29007/c3wqzbMath1403.68240arXiv1702.00847OpenAlexW2593389390MaRDI QIDQ4645725

Hans Tompits, Martin Suda, Armin Biere, Benjamin Kiesl, Martina Seidl

Publication date: 10 January 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1702.00847

zbMATH Keywords

first-order logicautomated reasoningautomated theorem provingSATpreprocessingblocked clausesclause elimination

Mathematics Subject Classification ID

Related Items (6)

Craig interpolation with clausal first-order tableaux ⋮ Truth Assignments as Conditional Autarkies ⋮ The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 ⋮ Set-blocked clause and extended set-blocked clause in first-order logic ⋮ Vampire getting noisy: Will random bits help conquer chaos? (system description) ⋮ SAT-Inspired Eliminations for Superposition

Uses Software

• TPTP

This page was built for publication: Blocked Clauses in First-Order Logic