化LF(X)中任一公式为可归约形式的算法

• 作者: 孟丹 宋振明 秦克云
• 来源期刊: 西南交通大学学报
• 学科: 数学
• 关键词: 人工智能 多值逻辑 自动推理 归结原理
• 年，卷（期）: 2003,（4）
• 页码范围: 433-437
• 页数: 5页
• 分类号: O141.1
• 字数: 2532字
• 语种: 中文
• DOI: 10.3969/j.issn.0258-2724.2003.04.014

摘要

针对基于归结方法的自动推理过程中的化任一公式为可归约形式这一问题进行研究.简述了LF(X)及其中公式的相关概念,证明了对LF(X)中公式进行转化的若干理论结果,并由此给出化LF(X)中任一公式为可归约形式的理论基础和基本算法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	宋振明	西南交通大学应用数学系	35	160	7.0	11.0
2	秦克云	西南交通大学应用数学系	147	930	15.0	22.0
3	孟丹	西南交通大学应用数学系	5	41	4.0	5.0