作　　者： ;

机构地区： 吉林大学计算机科学与技术学院

出　　处： 《计算机学报》 1988年第2期

摘　　要： 本文在布尔代数标准重写系统的基础上,提出了一种把一阶逻辑公式转换成布尔环中等式的方法,并由此建立了一阶逻辑的重写证明算法.这种算法可以充分利用环上的因子分解,证明过程中所产生的中间等式的数量也显著减少,对包含蕴涵符号的一阶逻辑公式尤为便利.

关 键 词： 布尔环 一阶逻辑 证明算法 因子分解 布尔代数 重写系统 最简式 证明过程 定理证明 语义树