On Quasi-Reductive and Quasi-Simplifying Deterministic Conditional Rewrite Systems.

Deterministic conditional rewrite systems permit extra variables on the right-hand sides of the rules. If such a system is quasi-reductive or quasi-simplifying, then it is terminating and has a computable rewrite relation. This paper provides new criteria for showing quasi-reductivity and quasi-simplifyingness. In this context, another criterion from [ALS94] will be rectified and a claim in [MAR96] will be refuted. Moreover, we will investigate under which conditions the properties exhibit a modular behavior. [ABSTRACT FROM AUTHOR]