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

A Mechanical Judge Method of the First-order Logic Formulas within the Limited Domain

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

The static, strict ＂physical symbol system＂ hypothesis made traditional artificial intelligence get into a difficult position for a time. The characteristics of flexibility and uncertanity of soft computing approach provided new ideas for the development of artificial intelligence, as a new building method of Computational Intelligence, soft computing is of great significance for the development of artificial intelligence.