Previous: Comparing the strength of propositional proof systems

Next: E-unification

Up: Supplementary Text Topics

Equational Term Rewrite Systems (ETRS's)

Although the search for interesting TRS's has enjoyed only limited success, the difficulties encountered in trying to automate equational theorem proving has given a major boost to the study of TRS's as one of the most promising methods to handle equality. Initial work was with group-like equations. However not many equational systems can be converted into TRS's, so some of the more recent work has been directed towards equational term rewrite systems (ETRS's),

When the has been specified then one refers to R as an -TRS.


When working with ETRS's the objective is, for a given set of equations E, to select a ``nice'' subset of E such that one has a normal form -TRS R with the crucial property that

Of course one wants a good algorithm to determine when the latter holds. There is very interesting work with rings, where consists of some associative and/or commutative laws.

Now let us look at some simple examples of normal form ETRS's for groups. Because of the popularity of the associative, resp. commutative, laws they are labelled A, resp. C, when referred to in the literature on ETRS's.

Note that the examples above are reduced. Here is some further reading.


EXERCISES

Since there are two binary operations in rings, we need to specify just which A and C laws for which operations are to go into .

 

For the remainder of the problems on rings AC denotes A and C for both + and . (We are working with commutative rings in each case).

For distributive lattices we take AC to refer to the associative and commutative laws for both operations.

Previous: Comparing the strength of propositional proof systems

Next: E-unification

Up: Supplementary Text Topics

Stan Burris
Fri Jan 31 11:34:57 EST 1997