基于语义tableau的一阶逻辑自动定理证明

• 作者: 刘全 孙吉贵
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 语义 tableau 有效性 完备性
• 年，卷（期）: 2005,（23）
• 所属期刊栏目: 博士论坛
• 页码范围: 22-24
• 页数: 3页
• 分类号: TP18
• 字数: 3480字
• 语种: 中文
• DOI: 10.3321/j.issn:1002-8331.2005.23.007

摘要

自动推理作为自动定理证明的扩展是人工智能研究的基础工作,许多重要的人工智能系统都是以推理系统为其核心部分,其中的tableau方法,由于具有通用性、直观性及易于计算机实现等特点,至今成为重要的自动推理方法之一.在tableau方法基础上,讨论了一阶逻辑中的自动定理证明理论,提出使用模型存在定理证明其可靠性和完备性的方法.同时也给出了带等词tableau方法的证明过程.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘全	苏州大学计算机科学与技术学院	99	1053	16.0	29.0
2	孙吉贵	吉林大学计算机科学与技术学院	134	2984	21.0	52.0