化LF(X)中任一公式为可归约形式的算法
针对基于归结方法的自动推理过程中的化任一公式为可归约形式这一问题进行研究.简述了LF(X)及其中公式的相关概念,证明了对LF(X)中公式进行转化的若干理论结果,并由此给出化LF(X)中任一公式为可归约形式的理论基础和基本算法.
作 者： 孟丹 宋振明 秦克云 作者单位： 西南交通大学应用数学系,四川,成都,610031 刊 名： 西南交通大学学报 ISTIC EI PKU 英文刊名： JOURNAL OF SOUTHWEST JIAOTONG UNIVERSITY 年，卷(期)： 2003 38(4) 分类号： O141.1 关键词： 人工智能 多值逻辑 自动推理 归结原理