Abstract:
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.