---
title: "Associative-Commutative Rewriting"
authors:
  - "Nachum Dershowitz"
  - "Jieh Hsiang"
  - "N. Alan Josephson"
  - "David A. Plaisted"
doi: ""
url: "https://ijcai.org/proceedings/1983/222"
pdf: "https://ijcai.org/proceedings/1983/0222.pdf"
venue: "Proceedings of the Eighth International Joint Conference on Artificial Intelligence"
year: 1983
pages: "940-943"
track: "Theorem Proving"
keywords:
---

# Associative-Commutative Rewriting

Nachum Dershowitz, Jieh Hsiang, N. Alan Josephson, David A. Plaisted

*Proceedings of the Eighth International Joint Conference on Artificial Intelligence*, pages 940-943.

## Abstract

We are currently extending the rewrite system laboratory REVE to ha ndle associative-commutative operators. In particul ar, we arc incorporating a set of rules for Boolean algebra that provides a refutationally-complete theorem prov er and a new progr a mming paradigm. To that end, we describe m et hods for proving termination of associativecommutativ e systems.