Strong Completeness of a Narrowing Calculus for Conditional Rewrite Systems with Extra Variables
Mohamed Hamada · Electronic Notes in Theoretical Computer Science · 2000
To simplify conditional narrowing, M. Hamada and A. Middeldorp [6] introduced the Lazy Conditional Narrowing Calculus (lcnc for short). In [6] and [7] lcnc was shown to be (strong) complete for various classes of conditional rewrite systems. In this paper we introduce two new completeness results for lcnc. We prove that lcnc is strong complete for terminating and level-confluent conditional term rewriting systems and lcnc is complete for level-complete conditional rewrite systems. In both results we do not assume any restrictions on the extra variables in the conditional rewrite systems.