10.1184/R1/6587564.v1 Kaustuv Chaudhuri Kaustuv Chaudhuri Frank Pfenning Frank Pfenning Greg Price Greg Price A Logical Characterization of Forward and Backward Chaining in the Inverse Method Carnegie Mellon University 1988 Inverse method Focusing SLD resolution Hyperresolution Intuitionistic linear logic 1988-01-01 00:00:00 Journal contribution https://kilthub.cmu.edu/articles/journal_contribution/A_Logical_Characterization_of_Forward_and_Backward_Chaining_in_the_Inverse_Method/6587564 The inverse method is a generalization of resolution that can be applied to non-classical logics. We have recently shown how Andreoli’s focusing strategy can be adapted for the inverse method in linear logic. In this paper we introduce the notion of focusing bias for atoms and show that it gives rise to forward and backward chaining, generalizing both hyperresolution (forward) and SLD resolution (backward) on the Horn fragment. A key feature of our characterization is the structural, rather than purely operational, explanation for forward and backward chaining. A search procedure like the inverse method is thus able to perform both operations as appropriate, even simultaneously. We also present experimental results and an evaluation of the practical benefits of biased atoms for a number of examples from different problem domains.