A logical characterization of forward and backward chaining in the inverse method (Q928660)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A logical characterization of forward and backward chaining in the inverse method |
scientific article |
Statements
A logical characterization of forward and backward chaining in the inverse method (English)
0 references
11 June 2008
0 references
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.
0 references
Inverse method
0 references
Focusing
0 references
SLD resolution
0 references
Hyperresolution
0 references
Intuitionistic linear logic
0 references