研究の紹介はじめに 項書き換えシステムの例 項書き換えシステムの完備性 グラス置き換えパズル グラス置き換えパズルの完備化 完備化手続き 群の完備化 両方向ペトリネットの完備化 組みひも問題の完備化 失敗無し完備化 おわりに はじめに 項書き換えシステム(term rewriting system)は等式にもとづく柔軟な計算法 と効率的な証明法を提供できるため，定理自動証明，関数型あるいは論理型言 語，代数的仕様記述，記号処理など，計算機科学のさまざまな分野で広くもち いられています． 項書き換えシステムは方向付けられた等式（書き換え規則）の集合として 定義されます．ところで，等式そのものにはもともと計算という意味はありま せん．たとえば，等式 1+2 = 3 は右辺と左辺が等価であるという論理的な意 味をもつだけです．したがって，論理の世界では，1+2 から 3 を得るだけ ではなく，逆に
