Kiesl, B., & Suda, M. (2017). A Unifying Principle for Clause Elimination in First-Order Logic. In L. de Moura (Ed.), Automated Deduction – CADE 26 : 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings. Springer Cham. https://doi.org/10.1007/978-3-319-63046-5_17
Preprocessing techniques for formulas in conjunctive normal form play an important role in first-order theorem proving. To speed up the proving process, these techniques simplify a formula without affecting its satisfiability or unsatisfiability. In this paper, we introduce the principle of implication modulo resolution, which allows us to lift several preprocessing techniques—in particular, several clause-elimination techniques—from the SAT-solving world to first-order logic. We analyze 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.
en
Additional information:
The final publication is available via <a href="https://doi.org/10.1007/978-3-319-63046-5_17" target="_blank">https://doi.org/10.1007/978-3-319-63046-5_17</a>.