Narrowing provides a complete procedure to solve equations modulo confluent and terminating rewriting systems. But it seldom terminates. This paper presents a method to improve th...
A term rewriting system is called complete if it is both confluent and strongly norrealizing. Barendregt and Klop showed that the disjoint union of complete term rewriting systems...