Video: |

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(A*B)==>i(B)*i(A). 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

?- equations_trs([X*(Y*Z)=(X*Y)*Z, e*X=X, i(X)*X=e], Rs), 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

Read

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