Focusing is traditionally seen as a means of reducing inessential non-determinism in backward-reasoning strategies such as uniform proof-search or tableaux systems. In this paper we construct a form of focused derivations for prepositional 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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Chaudhuri, K., & Pfenning, F. (2005). Focusing the inverse method for linear logic. In Lecture Notes in Computer Science (Vol. 3634, pp. 200–215). Springer Verlag. https://doi.org/10.1007/11538363_15
Mendeley helps you to discover research relevant for your work.