ACL2 Seminar, March 9, 2018

Speaker:
Benjamin Kiesl (TU Wien)

Title:
A Unifying Principle for Clause-Elimination in First-Order Logic

Abstract:
Preprocessing techniques for formulas in conjunctive normal form play
an important role in automatic theorem proving.  To speed up the
proving process, these techniques simplify a formula without affecting
its satisfiability or unsatisfiability.  In this talk, I discuss the
principle of implication modulo resolution, which can be used for
lifting several preprocessing techniques---in particular, several
clause-elimination techniques---from the SAT-solving world to
first-order logic.  I discuss confluence properties of these new
techniques and show how implication modulo resolution yields short
soundness proofs for the existing first-order techniques of predicate
elimination and blocked-clause elimination.