A logical characterization of forward and backward chaining in the inverse method (Q928660)

The authors present the focusing system for linear logic. The key feature of focusing is that each logical connective carries an intrinsic attribute, called polarity, that determines its behavior. Polarities may be chosen freely also for atomic propositions as long as duality is consistently maintained. The authors show that proof search on Horn propositions with the inverse method behaves either like hyperresolution or SLD resolution, depending on the chosen polarity for atoms. The focused inverse method therefore directly generalizes these two proof search strategies. Experimental results and an evaluation of the practical benefits of the method for a number of examples from different problem domains are presented.