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

https://hal.inria.fr/inria-00098410
Contributor : Publications Loria <>
Submitted on : Monday, September 25, 2006 - 4:53:29 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM

Identifiers

  • HAL Id : inria-00098410, version 1

Collections

Citation

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

Share

Metrics

Record views

172