| 化LF(X)中任一公式为可归约形式的算法 |
| |
| 引用本文： | 孟丹,宋振明,秦克云. 化LF(X)中任一公式为可归约形式的算法[J]. 西南交通大学学报, 2003, 38(4): 433-437 |
| |
| 作者姓名： | 孟丹 宋振明 秦克云 |
| |
| 作者单位： | 西南交通大学应用数学系,四川,成都,610031 |
| |
| 基金项目： | 国家自然科学基金 (6 0 0 74 0 14 ) |
| |
| 摘 要： | 针对基于归结方法的自动推理过程中的化任一公式为可归约形式这一问题进行研究．简述了LF(X)及其中公式的相关概念，证明了对LF(X)中公式进行转化的若干理论结果，并由此给出化LF(X)中任一公式为可归约形式的理论基础和基本算法．
|
| 关 键 词： | 人工智能 多值逻辑 自动推理 归结原理 |
| 文章编号： | 0258-2724(2003)04-0433-05 |
Algorithm of Transforming Any Formula in LF(X) into Reducible Form |
| |
| MENG Dan,SONG Zhen-ming,QIN Ke-yun. Algorithm of Transforming Any Formula in LF(X) into Reducible Form[J]. Journal of Southwest Jiaotong University, 2003, 38(4): 433-437 |
| |
| Authors: | MENG Dan SONG Zhen-ming QIN Ke-yun |
| |
| Abstract: | In the process of automated reasoning based on the resolution principle by compu ters, it is necessary to transform any formula into reducible form. The algorith m of transforming any formula in LF (X) is investigated. Based on the introdu ction of LF (X) and the related concepts, theoretic results for the transform ation are proved. Subsequently, the algorithm of transforming any formula in LF (X) into a reducible form is given. |
| |
| Keywords: | artificial intelligence multiple-value logic automated reasoning resolution principle |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
