Conditional narrowing modulo a set of equations (Q1261194)

Narrowing is a universal unification procedure for equational theories given by a canonical term rewrite system. We introduce conditional narrowing modulo a set of conditional equations and give a full proof of its correctness and completeness for equational conditional rewrite systems \(R\), \(E\) without extravariables where \(E\) is regular and \(R\), \(E\) is Church-Rosser modulo \(E\) and decreasing modulo \(E\). This result can be seen as the theoretical foundation of a special form of constraint logic and functional programming.