Abstract

In this paper we analyze completeness results for basic narrowing. We show that basic narrowing is not complete with respect to normalizable solutions for equational theories defined by confluent term rewriting systems, contrary to what has been conjectured. By imposing syntactic restrictions on the rewrite rules we recover completeness. We refute a result of Hoelldobler which states the completeness of basic conditional narrowing for complete (i.e. confluent and terminating) conditional term rewriting systems without extra variables in the conditions of the rewrite rules. In the last part of the paper we extend the completeness result of Giovannetti and Moiso for level-confluent and terminating conditional systems with extra variables in the conditions to systems that may also have extra variables in the right-hand sides of the rules.

BibTeX Entry

@article{MH-AAECC94,
 author    = "Aart Middeldorp and Erik Hamoen",
 title     = "Completeness Results for Basic Narrowing",
 journal   = "Applicable Algebra in Engineering, Communication and
              Computing",
 volume    = 5,
 volume    = "3-4",
 pages     = "213--253",
 year      = 1994,
 doi       = "10.1007/BF01190830"
}