Hypotheses Finding via Residue Hypotheses with the Resolution Principle

Abstract

For given logical formulae B and E such that B ⊭ E, hypothesis finding means the generation of a formula H such that B ⋀ H ⊨ E. Hypothesis finding constitutes a basic technique for fields of inference, like inductive inference and knowledge discovery. It can also be considered a special case of abduction. In this paper we define a hypothesis finding method which is a combination of residue hypotheses and anti-subsumption. Residue hypotheses have been proposed on the basis of the terminology of the Connection Method, while in this paper we define it in the terminology of resolution. We show that hypothesis finding methods previously proposed on the bases of resolution are embedded into our new method. We also point out that computing residue hypotheses becomes a lot more efficient under the restrictions required by the previous methods to be imposed on hypotheses, but that these methods miss some hypotheses which our method can find. Finally, we show that our method constitutes an extension of Plotkin’s relative subsumption.

In previous works [15],[16] by one of the authors, the bottom method was not well distinguished from inverse entailment.