@article{wirth-shallow-confluence,
year      ={2008},
author    ={Claus-Peter Wirth},
title     ={Shallow Confluence of Conditional Term Rewriting Systems},
journal   ={J. of Symbolic Computation},
publisher ={Elsevier},
url       ={http://dx.doi.org/10.1016/j.jsc.2008.05.005},
abstract  ={Recursion can be conveniently modeled with 
left-linear positive/negative-conditional term rewriting systems,
provided that non-termination, non-trivial critical overlaps, 
non-right-stability, non-normality, and extra variables are admitted. 
For such systems we present novel sufficient criteria for shallow confluence
and arrive at the first decidable confluence criterion admitting non-trivial
critical overlaps. 
To this end, we
restrict the introduction of extra variables of right-hand sides 
to binding equations 
and require the critical pairs to have somehow complementary
literals in their conditions. 
Shallow confluence implies level confluence,
has applications in functional logic programming, and 
guarantees the object-level consistency of the underlying data types
in the inductive theorem prover QUODLIBET.},
}