有穷客体域中一阶谓词公式的一种自动化判定法

摘要

本文给出了一个在自然数的有穷客体域Dk={1,2,…,k}(k≥0)内一阶谓词逻辑公式的k普遍有效性的判定算法.对于只包含一元谓词的公式以及对于带有前束量词(A)X1(A)2…(A)xm(E)y1(E)y2……(E)yn(m≥0,n≥0)且内部无自由变元的前束范式,该判定算法可判定这些公式的永真性,从而使该判定算法突破了有穷客体域以及k普遍有效性的局限.