An inference rule for hypothesis generation
Robert Demolombe, Luís Fariñas del Cerro · 1991
There are many new application fields for automated deduction where we have to apply abductive reasoning. In these applications we have to generate consequences of a given theory having some appropriate properties. In particular we consider the case where we have to generate the clauses containing instances of a given literal L. The negation of the other literals in such clauses are hypothesis allowing to derive L. In this paper we present an inference rule, called L-inference, which was designed in order to derive those clauses, and a L-strategy. The L-inference rule is a sort of Input Hyperresolution. The main result of the paper is the proof of the soundness and completeness of the L-inference rule. The L-strategy associated to the L-inference rule, is a saturation by level with deletion of the tautologies and of the subsumed clauses. We show that the L-strategy is also complete. 1