非古典論理における単純代入特性、及びそれのコンピューターへの応用の研究

点击翻译按钮获取中文摘要

非古典論理として具体的には、中間命題論理と様相命題論理を扱った。中間命題論理においては、高さが有限のクリプケモデルで特徴化されるものに対して、単純代入特性をもつための必要十分条件を与えることができた。この必要十分条件はモデルを使って与えたのだが、よく知られた結果を用いれば、公理的にも必要十分条件を与えることができ、かなり考えやすい条件となっている。また、それ以外の中間命題論理の中でも、かなりたくさんの論理に対して、単純代入特性をもつこと、あるいはもたないことを証明することができた。当初の目的のひとつに、「単純代入特性をもつかどうかをはっきりさせること」があったが、中間命題論理において、この目的はかなり達成できたと考えられる。これらの理論的裏づけを利用して、いくつかの中間命題論理においては、Theorem Proverを作成できた。さらに、これらのTheorem Proverを利用して、変数の数と論理記号の数を制限したときのリンデンバウム代数の構造など、中間命題論理におけるより詳しい事実を知ることができた。様相命題論理においても、高さが有限のクリプケモデルで特徴化されるものに対して、単純代入特性をもつための必要十分条件を与えることができた。様相命題論理においては、Theorem Proverはまだ作成されていないが、人工知能に役立つと考えられる分野なので、来年度申請中の科学研究費補助金または外部の助成金などで、是非とも完成させたい。またこれらの性質を、より応用的なマルチ様相論理や述語論理に対しても研究していきたいと考えている。