Skip to Main content Skip to Navigation

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 restriction- s 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.
Document type :
Complete list of metadatas
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:07:24 AM
Last modification on : Thursday, January 11, 2018 - 6:19:58 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:10:18 PM


  • HAL Id : inria-00072491, version 1



Jürgen Stuber. A Model-based Completeness Proof of Extended Narrowing And Resolution. [Research Report] RR-4135, INRIA. 2001, pp.18. ⟨inria-00072491⟩



Record views


Files downloads