@inproceedings{10.5555_1623516.1623594,
    author = {Dershowitz, Nachum and Hsiang, Jien and Josephson, N. Alan and Plaisted, David A.},
    title = {Associative-commutative rewriting},
    year = {1983},
    publisher = {Morgan Kaufmann Publishers Inc.},
    address = {San Francisco, CA, USA},
    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.},
    booktitle = {Proceedings of the Eighth International Joint Conference on Artificial Intelligence - Volume 2},
    pages = {940–944},
    numpages = {5},
    location = {Karlsruhe, West Germany},
    series = {IJCAI'83},
    date-added = {2026-1-25 10:50:3 +0100}
}

@inproceedings{10.5555_1623516.1623594, author = {Dershowitz, Nachum and Hsiang, Jien and Josephson, N. Alan and Plaisted, David A.}, title = {Associative-commutative rewriting}, year = {1983}, publisher = {Morgan Kaufmann Publishers Inc.}, address = {San Francisco, CA, USA}, 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.}, booktitle = {Proceedings of the Eighth International Joint Conference on Artificial Intelligence - Volume 2}, pages = {940–944}, numpages = {5}, location = {Karlsruhe, West Germany}, series = {IJCAI'83}, date-added = {2026-1-25 10:50:3 +0100} }