信念様相論理の効率的な部分系

概要

論文の詳細を見る
複数の人間の信念を表現し,推論する論理として様相論理の1つであるKD45(m)がある.しかし,この公理系は充足決定問題の計算量がP領域完全であるという問題点を持っている理由はこの論理の意味論である可能世界モデルの可能世界の数が入力に対して指数関数的に増大するためである可能世界の数を減らすような制限によって計算量を減らすことができる.本論文ではこのような2つの制限を提案し考察する1つ目の制限はKD45(m)に別の公理を加えたもの,2つ目は論理式の形を制限したものである.それぞれの制限は,可能世界の数を入力の長さに対して多項式的にしか増加しないように制約する.このことから充足決定問題の計算量がNP完全に下がることを示す.また,制限によって信念様相の否定に関する事実(すなわち,「分からない」に関する事実)の表現力が弱まる.それぞれ,「何重にもネストした信念についての事実が分からない」を表現できない,ネストした「分からない」を表現できないという制限が付く.「分からない」についての複雑な信念は人間にとっても推論するのが困難であり,めったに使われないため,この制限は妥当である.
一般社団法人情報処理学会の論文
1992-10-15