Sciweavers

Share
CSL
2005
Springer

Focusing the Inverse Method for Linear Logic

8 years 8 months ago
Focusing the Inverse Method for Linear Logic
Abstract. Focusing is traditionally seen as a means of reducing inessential nondeterminism in backward-reasoning strategies such as uniform proof-search or tableaux systems. In this paper we construct a form of focused derivations for propositional linear logic that is appropriate for forward reasoning in the inverse method. We show that the focused inverse method conservatively generalizes the classical hyperresolution strategy for Horn-theories, and demonstrate through a practical implementation that the focused inverse method is considerably faster than the non-focused version.
Kaustuv Chaudhuri, Frank Pfenning
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CSL
Authors Kaustuv Chaudhuri, Frank Pfenning
Comments (0)
books