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.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 1998, 142 (1), pp.102-126
Liste complète des métadonnées

Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 16:53:29
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58


  • HAL Id : inria-00098410, version 1



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



Consultations de la notice