変革による統一

Question

私は統一アルゴリズム="http://ja.wikipedia.org/wiki/abstract_syntax_tree" rel="nofollow"> ast 変換http://www.cambridge.org/gb/knowledge/isbn/item1166682 /？site_locale= en_gb "rel=" nofollow ">" TERMの書き換えとすべての "（Franz BaaderとTobias NipkowによってWoldcat ）。第4.6章変換による統一のために、それは例を持つ数学理論が多すぎ、私が好きだった限り明確ではありませんでした。

誰かが変換を利用するより単純な例を与えるか、または指摘することができます：

削除、分解、オリエント、除去。

Answer 1

削除：t = tは無意味であり、式のセットから削除できます。

1 =? 1 -> nil

.

Orient：すべての式をx =? tの形式で欲しいので、t =? xの形で任意の式を反転します。

2 =? x1 -> x1 =? 2

.

排除：x =? tを指定して、他のすべての方程式を変更してxのすべてのインスタンスをtに置き換えます。

x1 + x2 = 7, x2 = 5 -> x1 + 5 = 7, x2 = 5

.

分解：任意の機能を採用し、x =? tの形で方程式を取得する必要があります。このプロセスは技術的には一度に1つの関数を削除するだけです。

x1 + 5 = 7 -> x1 = 2
2 * (x1 + x2) = 14 -> x1 + x2 = 7

.

うまくいけばこれは助けます。