Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
B. Kiesl, M. Suda:
"A Unifying Principle for Clause Elimination in First-Order Logic";
Vortrag: CADE 26 - 26th International Conference on Automated Deduction,
Gothenburg, Sweden;
06.08.2017
- 11.08.2017; in: "Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings",
Springer,
Lecture Notes in Computer Science / 10395
(2017),
ISBN: 978-3-319-63046-5;
S. 274
- 290.
Kurzfassung englisch:
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.
Schlagworte:
theorem proving, first-order logic, sat, preprocessing, clause elimination, resolution
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-63046-5_17
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_264663.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.