A Model-based Completeness Proof of Extended Narrowing And Resolution

Jürgen Stuber 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We give a proof of refutational completeness for Extended Narrowing And Resolution (ENAR), a calculus introduced by Dowek, Hardin and Kirchner in the context of Theorem Proving Modulo. ENAR integrates narrowing with respect to a set of rewrite rules on propositions into automated first-order theorem proving by resolution. Our proof allows to impose ordering restrictions on ENAR and provides general redundancy criteria, which are crucial for finding nontrivial proofs. On the other hand, it requires confluence and termination of the rewrite system, and in addition the existence of a well-founded ordering on propositions that is compatible with rewriting, compatible with ground inferences, total on ground clauses, and has some additional technical properties. Such orderings exist for hierarchical definitions of predicates. As an exampe we provide such an ordering for a fragment of set theory.
Type de document :
Communication dans un congrès
R. Gore, A. Leitsch, T. Nipkow. First International Joint Conference on Automated Reasoning - IJCAR'2001, 2001, Siena, Italy, Springer, 2083, pp.195-210, 2001, Lecture notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00100440
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:45:25
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00100440, version 1

Collections

Citation

Jürgen Stuber. A Model-based Completeness Proof of Extended Narrowing And Resolution. R. Gore, A. Leitsch, T. Nipkow. First International Joint Conference on Automated Reasoning - IJCAR'2001, 2001, Siena, Italy, Springer, 2083, pp.195-210, 2001, Lecture notes in Computer Science. 〈inria-00100440〉

Partager

Métriques

Consultations de la notice

149