プログラムの性質のうちには，自然数やリストといったデータ構造に 関する帰納法で証明されるような性質があります． 例えば，リストを連結するappend関数は結合性---等式 app(xs,app(ys,zs)) = app(app(xs,ys),zs) が成立するという性質---をもちますが， この性質はリストxsの構造に関する帰納法を用いることで証明することが出来ます． このような性質を自動的に証明できれば， 記述したプログラムや仕様が意図した性質を持つかどうか調べることが簡単に出来ます． もし意図した性質が成立していなければプログラムや仕様がどこか間違っていたということですから， このようにしてプログラムや仕様を検証することができるわけです．
等式を対象とする論理を等式論理とよびます． 等式論理の枠組みでは，このような性質は帰納的定理という概念でとらえられています． そして，帰納的定理の自動証明法として， 項書き換えシステムをもとづく書き換え帰納法や潜在帰納法といった手法が知られています．
書き換え帰納法は項書き換えシステムにもとづく帰納的定理の自動証明法の1つです． 人が紙と鉛筆を使って証明を行なうときの方法とは異なり， 等式変形の方向性をあらかじめ指示した方向だけに制限することによって， より自動化に適した手法となっています．
書き換え帰納法では等式変形を一方向にだけ変形しますが， 可換性のようにそもそも両方向へ変形が可能な式の取り扱いが困難になってしまいます． そこで，方向性が簡単に決められないような等式を 書き換え帰納法で扱うための拡張を提案しました．
上にも述べたように， リストを連結するappend関数の結合性---等式 app(xs,app(ys,zs)) = app(app(xs,ys),zs) が成立する という性質---はリストxsの構造に関する帰納法で証明することが出来ます． ところが，とてもよく似た性質である， 同一のリストを連結する場合の結合性---等式 app(xs,app(xs,xs)) = app(app(xs,xs),xs) が 成立するという性質---を考えてみます． もちろん，より一般的な性質 app(xs,app(ys,zs)) = app(app(xs,ys),zs) が成立するわけですから， ys := xs, zs: = xs をとればこちらも成立するはずです． しかしながら，実際にリストxsの構造に関する帰納法で証明しようと試みると， 帰納法の仮定 app(xs,app(xs,xs)) = app(app(xs,xs),xs) が 証明したい等式 x:app(xs,app(x:xs,x:xs)) = x:app(xs,app(x:xs,x:xs)) に適用できる形になっていません． このため，帰納法の仮定が適用できず，証明に行き詰まってしまいます．
書き換え帰納法による自動証明でも同じような原因で証明が発散してしまいます． このような証明を成功させるには，適切な補題を証明の途中で追加する必要があります． 例えば，app(xs,app(xs,xs)) = app(app(xs,xs),xs) の場合には，より一般的な性質である app(xs,app(ys,zs)) = app(app(xs,ys),zs)) を補題として追加すれば， 後者の自動証明に先に成功し，もとの等式も導かれるわけです．
上記の補題生成は，等式の一般化による補題生成の例です． 上記の場合には一般化によって正しい等式が作られました． しかしながら，一般化によって正しくない等式が作られてしまうこともよくあります． (もともとの補題が正しい場合には)生成された補題も必ず正しいとき， その補題生成法を健全であるといいます． 健全な補題生成法の1例として健全一般化法が知られています． また，補題生成法の1つである発散鑑定法は健全でないことが知られていました． われわれは，発散鑑定法の一部を健全一般化法を置き換えることで， 健全な発散鑑定法が構成できることを明らかにしました．
本研究室では，これまで説明したようなさまざまな拡張を組みいれた 帰納的定理の自動証明システムを開発するとともに， より高機能な自動証明システムの実現を目指して新しい手法の提案や実験を行なっています． 下に示すのは，我々の研究室で開発している自動証明システムの実行スナップショットです．
まで．