シーケントを用いた証明計画法

概要

論文の詳細を見る
In a heuristic process of proof in mathematics, we try not only forward derivations from the assumptionssuch as `from A, we get B' but also backward derivations from the conclusion such as `in order to get A, we needB'. As the result, the order of the propositions in accomplished proof is different from the order in which we getthose propositions in the heuristic process. For planning of proof, it is important to express what we want to provenow and what we have got so far at each step in the heuristic process. However, this expression is different fromthe proof itself by the above reason. In this paper, we suggest a method of planning proof by using `sequents' forthe expression of assumptions and conclusions. For a concrete study, we use the first order NK system of Gentzento explain our method. Our method gives an algorithm to prove arbitrary tautologies of the first order NK system,and is also valid for practical mathematics which is not necessarily formalized in symbolic logic.
東京都立産業技術高等専門学校の論文