論理式の置換と選言標準形への変形による論理プログラムの計算手続き

概要

論文の詳細を見る
本論文では論理式の置換手続きと,等式の選言標準形(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