Associative-Commutative Rewriting
Abstract
We are currently extending the rewrite system laboratory REVE to handle associative-commutative operators. In particular, we are incorporating a set of rules for Boolean algebra that provides a refutationally-complete theorem prover and a new programming paradigm. To that end, we describe methods for proving termination of associative-commutative systems.
Cite
Text
Dershowitz et al. "Associative-Commutative Rewriting." International Joint Conference on Artificial Intelligence, 1983.Markdown
[Dershowitz et al. "Associative-Commutative Rewriting." International Joint Conference on Artificial Intelligence, 1983.](https://mlanthology.org/ijcai/1983/dershowitz1983ijcai-associative/)BibTeX
@inproceedings{dershowitz1983ijcai-associative,
title = {{Associative-Commutative Rewriting}},
author = {Dershowitz, Nachum and Hsiang, Jieh and Josephson, N. Alan and Plaisted, David A.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1983},
pages = {940-944},
url = {https://mlanthology.org/ijcai/1983/dershowitz1983ijcai-associative/}
}