電気・通信・電子・情報工学実験Dの説明

電気・通信・電子・情報工学実験D(電気・通信・電子・情報工学セミナー)は、 研究室に新たに配属された学部4年生に対して行われる実験で、 卒業研究のための基礎トレーニングのような位置づけとなります。 説明者(菊池)は、所属する研究室におけるこの実験を長年に渡って担当してきました。 内容は、普遍代数における語の問題を解くための手法である完備化とよばれる手続きを、 関数型プログラミング言語MLを用いて実装し、群の完備化などの実験を行うというものです。


(以下、電気・通信・電子・情報工学実験D実験指針より抜粋)

課題名:項書き換えシステムにもとづく自動証明

項書き換えシステムとは、方向付けられた等式(書き換え規則)の集合として定義される計算モデルである。 等式 t=s を複雑な式から単純な式への非可逆な一方向の書き換え規則 t→s とみなすと、 等式で記述された論理の世界を自然な形で計算の世界に結びつけることができる。 本実験では、項書き換えシステムにもとづく自動証明の手法として有名なKnuth-Bendix完備化手続きの実装を行う。 さらに、いくつかの例題の自動証明を実際に試み、その動作原理の理解を深めるとともに、 効率的な実装方法を考察する。
 1. 項書き換えシステムにもとづく自動証明の理論
 2. 項書き換えシステムの実装
 3. 完備化手続きの実装
 4. 自動証明実験と考察