# Prolog implementation of the Knuth-Bendix completion procedure

Prolog code: trs.pl

Trimmed to the essence (156 lines of code): poly.pl

 Video:

These files run with each of the following Prolog systems:
• SICStus Prolog 4.3.2
• SWI-Prolog 7.7.1
• GNU Prolog 1.4.4
For most of the mentioned systems, several lines can be removed, For example, in GNU Prolog, it is not necessary to include any libraries, so three directives can be removed.

Here is a version for SWI-Prolog, a freely available Prolog system where many predicates are already predefined and even more auxiliary definitions can be omitted: trs_swi.pl.

Read The Power of Prolog to understand the Prolog language features that are used in this code. In particular, I recommend the following chapters:

As an application of term rewriting, consider for example the completion of the group axioms:
```?- Es = [X*(Y*Z)=(X*Y)*Z, e*X=X, i(X)*X=e],
functors_order([*,e,i], Order),
completion(Es, Order, [], [], Rs),
maplist(portray_clause, Rs).
```
or shorter, using the interface predicate equations_trs/2 to relate a list of identities to a convergent term rewriting system:
```?- equations_trs([X*(Y*Z)=(X*Y)*Z, e*X=X, i(X)*X=e], Rs),
maplist(portray_clause, Rs).
```
This yields the following convergent TRS:
```i(B*A)==>i(A)*i(B).
A*i(A)==>e.
i(i(A))==>A.
A*e==>A.
A*B*C==>A*(B*C).
i(A)*A==>e.
e*A==>A.
i(A)*(A*B)==>B.
i(e)==>e.
A*(i(A)*B)==>B.
```
We can use this TRS to reduce—for example—the term X*i(X) to its normal form:
```?- normal_form(\$Rs, X*i(X), NF).
Gs = ...,
Rs = ...,
NF = e .
```
This shows that the left-inverse is also a right-inverse in groups!

To decide equality between any two terms in groups, simply reduce both of them to their respective normal forms, and see whether they are identical. This only takes a finite number of steps, since the TRS is convergent and hence terminating.

Note: In the above example, \$Rs reuses the rules Rs from the preceding query. If your Prolog toplevel does not provide this feature, please form the conjunction of the two queries instead, using Rs directly instead of referencing it with the symbol \$.