纯蕴涵演算定理证明的两个能行过程

Two Effective Processes for Theorem Proving in Pure Implication Calculus

以不同于通常的根先证明搜索策略,从纯蕴涵演算的初始公理和初始规则出发,通过分析公理在定理证明中的作用和规律,可以得到两个实用的能行过程。这两个能行过程虽不是机械化的证明搜索程序,但有助于新程序的研发,并且可应用于数理逻辑的实际教学。

There are two practical effective processes for theorem proving based on the primitive axioms and rules of pure implication calculus. They both result from analyzing the role of axioms in theorem proving,and are different from the usual root-first proof search strategies. These two processes are not mechanical procedures for proof search,but helpful for the development of these procedures and for the practical teaching of mathematical logic.