任意矩阵的连接法中的简化规则

连接法的基本思想是证明矩阵中每一条路径都是互补的,即至少含有一个互补文字对,如果所有的路径是互补的则矩阵是互补的。因而原始待证公式是有效的,在[1]中W.Bibel给出了一阶逻辑的规范矩阵算法,这个算法容易推广到任意矩阵中。 作者在[2]中提出了几条应用于规范矩阵连接法的简化规则,本文提出两条可用于任意矩阵连接法的简化规则,它们的使用使得连接证明中要测试的路径和子目标的个数减少,并保证了原来矩阵的互补性。这两条规则作为定理来叙述并加以证明。