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

• 作者: 王宗亮
• 来源期刊: 电脑与电信
• 学科: 工学
• 关键词: 人工智能 自动定理证明 一阶谓词 判定法
• 年，卷（期）: 2006,（6）
• 所属期刊栏目: 理论研究
• 页码范围: 13-18
• 页数: 6页
• 分类号: TP3
• 字数: 5432字
• 语种: 中文
• DOI: 10.3969/j.issn.1008-6609.2006.06.003

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王宗亮	广东水利电力职业技术学院计算机信息工程系	5	5	1.0	2.0