| 一种新的基于假设的自然推理系统 |
| |
| 引用本文： | 张学平,邵军力,王元元,程翼羽.一种新的基于假设的自然推理系统[J].解放军理工大学学报,1992(2). |
| |
| 作者姓名： | 张学平 邵军力 王元元 程翼羽 |
| |
| 作者单位： | 浙江大学 |
| |
| 摘 要： | 本文在介绍自动定理证明的历史和分析自然推理研究的现有成果的基础上,提出了用以实现启发式自然推理系统HNDS的确定性推理算法。并设计了用作推理基本手段的假设机制。本系统采用知识库系统的软件结构,面向标准形式的命题逻辑和一阶谓词逻辑,对系统定理能给出清晰的类人证文过程。HNDS系统基于的推理算法理论上是合理的和完备的,这主要因为系统结合了自然推理与消解原理,并首创了量词逐层Skolem化的策略。
|
| 关 键 词： | 自动定理证明(ATP) 自然推理 消解原理 假设 一阶谓词逻辑 |
A Novel Hypothesis-based Natural Deduction System |
| |
| Zhang Xueping Shao Junli Wang Yuanyuan Cheng Yiyu.A Novel Hypothesis-based Natural Deduction System[J].Journal of PLA University of Science and Technology(Natural Science Edition),1992(2). |
| |
| Authors: | Zhang Xueping Shao Junli Wang Yuanyuan Cheng Yiyu |
| |
| Institution: | Zhejiang University |
| |
| Abstract: | Based on the review of the history of automatic reasoning and the evaluation of several well-known natural deductive systems, this paper presents a novel hypothesis-based heuristic natural deductive sytem(HNDS), in which the hypothesis is used as the fundamental means of deduction. The determinate reasoning algorithm and relevant hypothesis mechanism are given. The implementation of HNDS shares the software architecture of knowledge base system. In our system, the resolution principle is incorporated and the guantifiers are deleted only when needed. The present HNDS can give man-like proof for the system theorem, and the determinate reasoning algorithm is sound and complete. |
| |
| Keywords: | automatic theorem proving natural deduction resolution principle hypothesis first order predicate logic |
| 本文献已被 CNKI 等数据库收录！ |
