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 Hölldobler 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. 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

@inproceedings{MH-ALP92,
 author    = "Aart Middeldorp and Erik Hamoen",
 title     = "Counterexamples to Completeness Results for Basic Narrowing",
 booktitle = "Proceedings of the 3rd International Conference on Algebraic
              and Logic Programming",
 series    = "Lecture Notes in Computer Science",
 volume    = 632,
 pages     = "244--258",
 year      = 1992,
 doi       = "10.1007/BFb0013830"
}