従来の論理計算の理論体系は、一階述語論理式で書かれた証明問題を推論によって解くことが基本になっている。しかし、解くことのできる証明問題は、組み込み述語を使わないものに限られている。さらに求解問題を解く理論も十分でない。本研究は、従来の証明問題中心の理論を脱皮して、求解問題中心の理論へ、そしてモデルインターセクション問題中心の理論へ拡大飛躍した。この理論は、① 新しいロジックであるKRロジック、② 新しい問題クラスであるモデルインターセクション問題、③ 新しい計算を生み出す等価変換、という枠組みを確立し、論理学と論理計算を歴史的に新たな段階へと発展させるものである。
|