Carnegie Mellon University
Browse

Focusing the Inverse Method for Linear Logic

Download (94.48 kB)
journal contribution
posted on 2012-08-01, 00:00 authored by Kaustuv Chaudhuri, Frank Pfenning
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 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.

History

Date

2012-08-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC