FC2ブログ
--.--
--
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

07.05
Sat
導出原理を使って自動定理証明系を書いているわけですが、
純粋な導出原理のみの実装だと扱いにくくなる論理式があります。式が等号を含んでいる場合です。

導出原理はパターンマッチによって相補的になるリテラルの除去を繰り返し行うだけで特別な論理式
(推論の効率的な意味で特別に扱うべき式、つまり等号を含んでいるものという意味)
について特別な処理を行うことはしません。あたりまえですね。
述語記号が等号であっても、等号に固有な性質を考慮した推論は行うことができない
つまり、単なる二項述語としての扱いしかしません。

これを解決する方法がいくつかあります。

まず、特別扱いする方法ではなくて単に等号公理を入れる方法を見てから
それをベースに導出原理の拡張を考えてみます。

以下を公理として入れてしまえば、等号に関する論理式が証明できます

(Pが全てのn引数の述語を暗黙に表しているという問題がある。つまり高階論理)
(上と同じ問題はある)
証明したい式が等号を含む場合は常にこれらの公理を考えることになり効率は当然よくありません。
定理証明において(というか何でも)効率が良くない、要するに探索空間を爆発させてしまうやり方は
有限時間内で証明できる式の範囲を狭めかねませんのでよろしくありません。

ところで等号公理の下2つが表す事は何かというと、"等しいもの"同士は置き換えが効くという置換の規則を
表しているように考えられます。なのでこれをもとに導出原理を拡張したのがParamodulation法です。
正確な定義は述べませんが、やっている事は簡単でからを導くというもので、
これで導出原理を拡張します。
ところがParamodulationはあまり効率の良くないアルゴリズムです。なぜかを説明すると上の簡単な例だと置き換えられる場所つまり中の項として現れるのは一箇所だけですが(というか1引数の述語なので)、
一般には複数ヶ所に現れますし、更に項が関数項ならその中にも出現する可能性があります。
この場合どこをに置き換えたらいいのでしょうか?
もし全てのパターン数だけ、新たな節が生成されたらかなり厄介です。

そして3つ目の方法。等号を書き換え規則として考えるのは前2つと同じものでKnuth-Bendixの完備化アルゴリズムというのがあり、これが等式の証明に使えます。がこれは次回にまとめたいと思います。
スポンサーサイト

comment 0 trackback 0
トラックバックURL
http://telracsmoratori.blog.fc2.com/tb.php/188-61d3d383
トラックバック
コメント
管理者にだけ表示を許可する
 
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。