Go to page
 

Bibliographic Metadata

Title
A Unifying Principle for Clause Elimination in First-Order Logic
AuthorKiesl, Benjamin ; Suda, Martin
Published in
Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings / de Moura, Leonardo, Springer, Cham, 2017, page 274-290
Published2017
Edition
Accepted version
LanguageEnglish
SeriesLecture Notes in Computer Science ; 10395
Document typeArticle in a collected edition
Keywords (EN)theorem proving / first-order logic / sat / preprocessing / clause elimination / resolution
Project-/ReportnumberERC Starting Grant 2014 SYMCAR 639270
Project-/ReportnumberAustrian Science Fund (FWF): W1255-N23
Project-/ReportnumberAustrian Science Fund (FWF): S11403-N23
Project-/ReportnumberAustrian Science Fund (FWF): S11409-N23
Project-/ReportnumberNational Science Foundation (NSF): CCF-1618574
ISBN978-3-319-63046-5
URNurn:nbn:at:at-ubtuw:3-3321 Persistent Identifier (URN)
DOI10.1007/978-3-319-63046-5_17 
Restriction-Information
 The work is publicly available
Files
A Unifying Principle for Clause Elimination in First-Order Logic [0.25 mb]
Links
Reference
Classification
Abstract (English)

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 techniquesin particular, several clause-elimination techniquesfrom 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.

Note
Stats
The PDF-Document has been downloaded 19 times.