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

02.18
Tue

自動定理証明系、その基礎に当たる導出原理とかについて。

エルブランの定理は、任意の恒真な一階述語論理式について成り立つものなのだそうですが、

ウィキペディアにあるように対象とする論理式は予め冠頭標準形であるとして(変換できるとして)

説明してる本が多いと思います。

実際、導出原理で節集合を求めるときに母式に量化記号が入っていると、やっかいな事になります。

一般的に節の定義をリテラルの選言とするから、量化記号は邪魔なのです。

そこで冠頭標準形でない論理式について、導出原理を使うには一連の変換作業が必要になります。


さてそこで、任意の一階述語論理式を冠頭標準形に変形するツールを書いてみました。

githubにソース置いてぽーいだとあれなので、ウェブのフォームよりできますのでどうぞ

一階述語論理式の標準形

自宅のサーバで動かしてるツールなので突然アクセスできなくなってることがあるかもですご了承下さい...


論理式を冠頭標準形に変換して、なおかつ母式部分を連言(乗法)標準形、

または選言(加法)標準形のいずれかにすることができます。

冠頭形にする際に束縛変数は一意性を保つためにvar_をプリフィックスとする数字に置き換えられますので注意下さい。


また、命題論理式でも標準形に変形することができます。

その場合冠頭形とかいう概念はないので、CNF形またはDNF形の何れかにできます。


スポンサーサイト

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