Let E be any given equational theory not necessarily admitting a finite 
canonical system. One knows then, that ordered completion is adequate for 
proving valid (equational) E-theorems.
This is so, since it generates a final system which is ground canonical, if 
the reduction ordering employed is a cso. The same fact also leads to a 
rather loose conclusion that narrowing techniques must suffice for E-unication, 
when combined with ordered completion. In this work, we found such a 
conclusion on a clear basis, by giving an inference system which also allows 
the narrowing to be basic. Our inference rules are expressed in a setting of 
constraints, allowing our initial equations to be constrained too. We will 
be assuming however, to be working only with equality, or ordering constraints.
Our approach, though inspired by the earlier works of [KKR90], [NR92], uses 
a slightly different notion of constrained rewriting. This helps us arrive 
at the following conclusions:
- If tau is any solution of the unicand s ?= t, then our basic narrowing 
under ordered completion generates a sigma more general than tau.
- If the initial equations are without constraints, the superposition in our 
ordered paramodulation inferences is basic too.
- The unicands can always be kept in normal form.
- If (some of) the initial equations are constrained, our approach needs to 
resort to some propagation'in the sense of [KKR90] to remain complete; 
but this is needed only wrt the initial constraints.

The ordered completion part of our approach may thus be viewed as extending 
the results of [NR92], to allow for intial constraints. The ground confluence 
of our 'final system' S, as well as the completeness of our narrowing, are 
proved by establishing that any S-step between any two ground terms s, t, can 
be replaced by an (innermost) S-chain between s, t with S-normal matches all 
along.

References
[KKR90] C. Kirchner, H. Kirchner, and M. Rusinowitch. Deduction with symbolic 
constraints. Revue d'Intelligence Articielle, 4(3):9-52, 1990. Special issue 
on automatic deduction.
[NR92] R. Nieuwenhuis and A. Rubio. Basic superposition is complete. 
In proceedings 11th international conference on automated deduction, Albany 
(NY, USA), volume 617 of lecture notes in artificial intelligence. 
Springer-Verlag 1992.