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

非经典逻辑简单赋值性质及其在计算机中的应用研究

• 批准号: 05740144
• 负责人: 佐々木 克巳
• 金额: $ 0.19万
• 依托单位: Nanzan University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1993
• 资助国家: 日本
• 起止时间: 1993 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-05740144/
• 关键词: 非古典論理; 中間命題論理; 様相論理; 単純代入特性; Theorem Prover

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

The theory of non-classical theory is related to the specific theory of life and life. In the middle of the problem, it is necessary to apply the necessary conditions for the special operation of the system, the transfer of properties, and the necessary conditions for the transfer of properties. It is necessary to use the necessary conditions to make sure that the conditions are correct, that the results of the axioms are not necessary, and that the conditions are correct. In other words, you need to know that you are in the middle of the problem, and that you are not allowed to do so, and that you are not allowed to do so. In the first place, the purpose of the system is to change the characteristics of the system, and the purpose is to change the quality of the property. The theory of computer science makes use of the problem of life management and Theorem Prover in the theory of information technology. In this paper, we use the number of data, the number of Theorem Prover, the number of data, the number of records, the number of records, the number of records You need to know each other that you need to know that you are going to have a problem with each other, that is, you are going to have a problem with each other, and you are going to have a lot of information about what is necessary and what is necessary. In order to solve each other's problems, the Theorem Prover system has been built into a research program, an artificial knowledge system, an examination program, an application for scientific research grants in the coming year, an external grant program, and a non-financial assistance program. The relationship between sex and sex is described in this paper, which is used in the study of sex and sex.

项目成果

Katsumi SASAKI: "The simple substitution property of the intermedlate propositional logics onfinite slices" Studia Lagica. 52. 41-62 (1993)

Katsumi SASAKI：“有限切片中间命题逻辑的简单替换性质”Studia Lagica。