RLD演绎及子句蕴含与子句包含关系的非等价性

软件复用的一个主要任务是可复用软件构件的表示与检索，由于一阶逻辑能够描述软件构件的计算语义，因此用一阶逻辑表示构件及用基于归结原理的自动定量证明技术检索构件的研究在软件工程领域得到了足够的重视，为了简化基于演绎的构件检索技术的程序设计结构及提高演绎效率，提出了最右线性演绎RLD（rightmost linear deduction)，并证明了它的完备性，同时，指出了子句蕴含与子句包含关系的非等价性，并给出了由子句蕴含关系推出子句包含关系成立的一个充分条件。

RLD DEDUCTION AND NON-EQUIVALENCE BETWEEN CLAUSE-IMPLICATION AND CLAUSE-SUBSUMPTION

One of the main issues of software reuse is to represent software component and develop relevant retrieval technique. Because the first order logic can characterize the computational semantics of a software component, it has become an important research direction in software engineering domain to use first order logic to represent a component and to use resolution based automatic theorem proving technology to retrieve it. In order to simplify the programming structure of deduction based component retrieval and improve the deduction efficiency, the RLD deduction (rightmost linear deduction) is proposed and its completeness is proved in this paper. At the same time, the non equivalence between clause implication and clause subsumption is pointed out and a sufficient condition that makes the proposition, i.e., clause implication implies clause subsumption, is proposed.