論理式の置換と選言標準形への変形による論理プログラムの計算手続き
スポンサーリンク
概要
- 論文の詳細を見る
本論文では論理式の置換手続きと,等式の選言標準形(DNF)への変形手続きを組み合わせた論理プログラムの計算手続きの改良について述べる.改良前の手続きは,論理プログラムとして任意のFirstt-order Logic Program (FLP)を,ゴールとして任意の1階論理プログラムをとることができ,FLPと2値論理で同値な完備プログラム(FLPの完備化)の3値論理での論理的帰結を健全かつ完令に判定できる.言い換えると,FLPの2値論理での論理的帰結の中に,この手続きでは判定できないものが存在する.しかし,論理式の置換方法を改良することによって,FLPの2値論理での論理的帰結をより多く判定できるようになり,また,DNFへの変形手続きを引き続き用いることによって,ゴールがFLPの論理的帰結となる自由変数の値を表現するDNFを計算できるという手続きの特徴を維持できる.本論文では,改良された論理式の置換方法を提示し,この方法を用いた計算手続きはFLPの2値論埋での論理的帰結を改良前の手続きよりも真に多く判定できることを示す.また,この手続きはFLPの完備化とは異なる完備プログラムの3値論理での論理的帰結を健全かつ完全に判定できることを証明する.
- 2003-03-01
論文 | ランダム
- Composite likelihood-based meta-analysis of breast cancer association studies
- Microwave coagulation versus sclerotherapy after band ligation to prevent recurrence of high risk of bleeding esophageal varices in Child-Pugh's A and B patients
- 集団の形成とそのもつ力 (現代社会における集団とは)
- 513 幼児の遊戯場面の観察(3) : 遊び構造の年齢による差異(500 社会性と人間関係)
- 20 遊戯場面の観察(2) : 遊戯場面の観察の方法論的検討(2.発達(幼児))