Church-Rosser Properties of Weakly Terminating Term Rewriting Systems
Proceedings of the Eighth International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 909-914.
Abstract
The well known Knuth and Bendix completion procedure computes a convergent term rewriting system from a given set of equational axioms. This procedure was extended to handle mixed sets of rules and equations in order to deal with axioms that cannot be used as rules without loosing the required termination property. The developed technique requires the termination property of the rules modulo the equations. We describe here an abstract model of computation, assuming the termination property of the set of rules only. We show that two abstract properties, "uniform confluence modulo" and "uniform coherence modulo" are both necessary and sufficient ones to compute with these models. We then give sufficient properties that can be checked on "parallel critical pairs", assuming the rules are left linear. These results allow to deal with sets of axioms including commutativity, associativity and idempotency.
@inproceedings{ijcai1983p214,
title = {Church-Rosser Properties of Weakly Terminating Term Rewriting Systems},
author = {Jouannaud, Jean-Pierre and Kirchner, Hélène and Rémy, Jean-Luc},
booktitle = {Proceedings of the Eighth International Joint Conference on
Artificial Intelligence, {IJCAI-83}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Alan Bundy},
pages = {909--914},
year = {1983},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1983/214},
}
TY - CPAPER TI - Church-Rosser Properties of Weakly Terminating Term Rewriting Systems AU - Jouannaud, Jean-Pierre AU - Kirchner, Hélène AU - Rémy, Jean-Luc T2 - Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83 PB - International Joint Conferences on Artificial Intelligence PY - 1983 SP - 909 EP - 914 UR - https://ijcai.org/proceedings/1983/214 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
