HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Local simplification

Christopher Lynch 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a modification to the paramodulation inference system, where semantic equality and non-equality literals are stored as local simplifiers with each clause. The local simplifiers are created when new clauses are generated and inherited by the descendants of that clause. Then the local simplifiers can be used to perform demodulation and unit simplification, if certain conditions are satisfied. This reduces the search space of the theorem proving procedure and the length of the proofs obtained. In fact, we show that for ground SLD resolution with any selection rule, any set of clauses has a polynomial length proof. Without this technique, proofs may be exponential. We show that this process is sound, complete, and compatible with deletion rules (e.g., demodulation, subsumption, unit simplification, and tautology deletion), which do not have to be modified to preserve completeness. We also show the relationship between this technique and model elimination.
Document type :
Journal articles
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Monday, September 25, 2006 - 4:53:29 PM
Last modification on : Friday, February 4, 2022 - 3:30:13 AM


  • HAL Id : inria-00098410, version 1



Christopher Lynch. Local simplification. Information and Computation, Elsevier, 1998, 142 (1), pp.102-126. ⟨inria-00098410⟩



Record views