论文部分内容阅读
本文给出了一个在自然数的有穷客体域Dk={l，2，…，k}（k≥0）内一阶谓词逻辑公式的k普遍有效性的判定算法。对于只包含一元谓词的公式以及对于带有前束量词A↓X1A↓2…AxmЗy1Зy2…Зyn（m≥0，n≥0）且内部无自由变元的前束范式，该判定算法可判定这些公式的永真性，从而使该判定算法突破了有穷客体域以及k普遍有效性的局限。