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

Classical first-order logic (03B10) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

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