| 基于格值一阶逻辑LF（X）的自动推理算法 |
| |
| 引用本文： | 李晓冰,徐扬.基于格值一阶逻辑LF（X）的自动推理算法[J].计算机工程与应用,2010,46(23):18-20. |
| |
| 作者姓名： | 李晓冰 徐扬 |
| |
| 作者单位： | 1. 东北财经大学,管理科学与工程学院,辽宁,大连,116025
2. 西南交通大学,智能控制开发中心,成都,610031 |
| |
| 基金项目： | 国家自然科学基金，高等学校博士学科点专项科研基金项目 |
| |
| 摘 要： | 基于谓词逻辑的归结推理方法是目前理论上较为成熟、可以在计算机上实现的推理方法之一。针对格值一阶逻辑LF(X)中归结自动推理问题，以格值一阶逻辑LF(X)的α-归结原理为理论基础，通过对例子进行分析，提出了LF(X)中简单广义子句集的归结自动推理算法，并证明了该算法的可靠性和完备性。
|
| 关 键 词： | 格值一阶逻辑 自动推理 α-归结原理 简单广义子句集 |
| 收稿时间： | 2010-5-10 |
| 修稿时间： | 2010-6-28
|
Automated reasoning algorithm based on lattice-valued first-order logic LF(X) |
| |
| LI Xiao-bing,XU Yang.Automated reasoning algorithm based on lattice-valued first-order logic LF(X)[J].Computer Engineering and Applications,2010,46(23):18-20. |
| |
| Authors: | LI Xiao-bing XU Yang |
| |
| Affiliation: | 1.Department of Management Science and Engineering,Dongbei University of Finance and Economics,Dalian,Liaoning 116025,China 2.Intelligent Control Development Center,Southwest Jiaotong University,Chengdu 610031,China |
| |
| Abstract: | Resolution reasoning method based on predicate logic is one of methods which are well-developed and can be implemented on computer.In order to solve automated reasoning based on resolution principle in lattice-valued first-order logic,a resolution automated reasoning algorithm based on α-resolution principle in lattice-valued first-order logic is proposed by analyzing an example.Its soundness and completeness are proved. |
| |
| Keywords: | lattice-valued first-order logic automated reasoning α -resolution principle simple generalized clause set |
| 本文献已被 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
