Trimmed to the essence (156 lines of code):

Video: |

These files run with

- SICStus Prolog 4.3.2
- SWI-Prolog 7.7.1
- GNU Prolog 1.4.4

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:

Read

As an application of term rewriting, consider for example the completion of the

?-or shorter, using the interface predicateEs = [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).

?-This yields the followingequations_trs([X*(Y*Z)=(X*Y)*Z, e*X=X, i(X)*X=e], Rs), maplist(portray_clause, Rs).

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

?- normal_form($Rs, X*i(X), NF). Gs = ..., Rs = ...,This shows that the left-inverse is also a right-inverse in groups!NF = e.

To

Please write to triska@metalevel.at if you have any questions about this code or any other aspects.