定理証明在M-6800机上的实現

本文介绍了在M-6800微型机上,用BASIC语言实现定理证明的过程。证明过程所采用的方法是线性归结的特殊情形——单位归结。在证明过程中,我们采用了支撑集、包括检查等技巧,使得演绎探索中的冗余信息大为减少,提高了证明的效率。