A MACHINE-ORIENTED LOGIC BASED ON RESOLUTION PRINCIPLE
A MACHINE-ORIENTED LOGIC BASED ON RESOLUTION PRINCIPLE
复制标题
DOI：
10.1145/321250.321253
复制
发表时间：
1965-01-01
影响因子：
2.5
通讯作者：
ROBINSON, JA
中科院分区：
文献类型：
--
作者：
ROBINSON, JA
阿贡纳里昂实验室 * 和t~ ice U. niver~ itg~：tb.~道。本文研究了利用Herbrand关于一阶谓词etdeulus的基本定理在计算机上进行定理证明的方法，以期提高这些方法的效率，扩大其实用范围。对替换过程（变量项）的elose分析，以及对这种替换的结果进行真值函数分析的过程，揭示了这两个过程可以组合成一个新的过程（称为解析），迭代比由替换阶段与真值函数分析阶段交替组成的旧循环过程更有效。归结过程的理论是以一阶逻辑系统的形式提出的。只有一个推理原则（决议原则）。证明了系统的完备性，基于系统的最简单的证明过程就是完备性证明的直接实现。然而，这种证明过程效率很低，本文最后讨论了几个原则（称为搜索原则），它们适用于设计以归结为基本逻辑过程的有效证明过程.本文介绍了一种一阶逻辑公式，它是专门为计算机定理证明程序的基本理论工具而设计的。早期的定理证明程序是基于一阶逻辑系统的，这些系统最初是为其他目的而设计的。这些逻辑系统的一个突出特点是它们的推理原则相对简单，这一点在本文所描述的系统中得到了体现。传统上，由于实用和心理的原因，演绎中的一个小步骤被要求足够简单，广义地说，在一个单一的智力行为中被人理解为正确的。毫无疑问，这一习惯的出发点是希望演绎的每一个步骤都是不容置疑的，即使整个演绎可能由一长串这样的步骤组成。一个演绎的最终结论，如果这个演绎是正确的，那么它是从演绎中所使用的前提逻辑地得出的;但是人类的心灵可能很好地适应了从前提到结论的直接过渡，这一过渡令人惊讶，因此（心理上）是可疑的。对演绎推理的逻辑分析的一部分观点，即盗窃，是把复杂的推理，把超出人类思维能力的单个步骤，简化为简单推理的链条，其中每一个都在人类思维能力的范围内，作为一个单一的处理来理解。
Argonne Nalionrd Laboratory* and t~ ice U. niver~ itg~: tb.~ tract. Theorem-proving on the computer, using procedures based on the fund~-mental theorem of Herbrand concerning the first-order predicate etdeulus, is examined with~ view towards improving the efticieney and widening the range of practical applicability of these procedures. A elose analysis of the process of substitution (of terms for variables), and the process of truth-functional analysis of the results of such substitutions, reveals that both processes can be combined into a single new process (called resolution), iterating which is vastty more ef [ieient than the older cyclic procedures consisting of substitution stages alternating with truth-functional analysis stages. The theory of the resolution process is presented in the form of a system of first<~ rder logic with. just one inference principle (the resolution principle). The completeness of the system is proved; the simplest proof-procedure based oil the system is then the direct implementation of the proof of completeness. Howew~ r, this procedure is quite inefficient,~ nd the paper concludes with a discussion of several principles (called search principles) which are applicable to the design of efficient proof-procedures employing resolution as the basle logical process.1. introductionPresented in this paper is a formulation of first-order logic which is specifically designed for use as the basle theoretical instrument of a computer theoremproving program. Earlier theorem-proving programs have been based oil systems of first-order logic which were originally devised for other purposes. A prominent feature of those systems of logic, which is l~ eking in the system described in this paper, is the relative, simplicity of their inference principles. Traditionally, a sirlgle step in a deduction has bee~ required, for pragmatic a,~ d psychological reasons, to be simple enough, broadly speaking, to be apprehended as correct by a human being in a single intellectual act. No doubt this custom origiu~ tes i~ 1 the desire that each single step of a deduction should be indubitable, even though the deduction as a whole may consist of a long chain of such steps. The ultimate conclusion of a deduction, if the deduction is correct, follows logie~ dly from the premisses used ia tile deduction; but the human mind may well fit~ d the unmediated transition from the prelnisses to the conclusion surprising, hence (psychologically) dubitable. Part of the point, theft, of the logical analysis of deductive reasoning has been to reduce complex inferences, which are beyond the capacity of the human mind to grasp as single steps, to chains of simpler inferences, each of which is within the capacity of the human milld to grasp as a single transactiom