Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00100440
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 2:45:25 PM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM

Identifiers

  • HAL Id : inria-00100440, version 1

Collections

Citation

Jürgen Stuber. A Model-based Completeness Proof of Extended Narrowing And Resolution. First International Joint Conference on Automated Reasoning - IJCAR'2001, 2001, Siena, Italy, pp.195-210. ⟨inria-00100440⟩

Share

Metrics

Record views

347