Focusing the inverse method for linear logic

Kaustuv Chaudhuri; Frank Pfenning

doi:10.1007/11538363_15

Focusing the inverse method for linear logic

Kaustuv Chaudhuri, Frank Pfenning

Carnegie Mellon University

Research output: Contribution to journal › Conference article › peer-review

Abstract

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.

Original language	English
Pages (from-to)	200-215
Number of pages	16
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3634
DOIs	https://doi.org/10.1007/11538363_15
Publication status	Published - 1 Jan 2005
Externally published	Yes
Event	19th International Workshop on Computer Science Logic, CSL 2005 and 14th Annual Conference of the EACSL - Oxford, United Kingdom Duration: 22 Aug 2005 → 25 Aug 2005

Access to Document

10.1007/11538363_15

Cite this

@article{3421df7d75ee4deba2c3f4460c09b15b,

title = "Focusing the inverse method for linear logic",

abstract = "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.",

author = "Kaustuv Chaudhuri and Frank Pfenning",

year = "2005",

month = jan,

day = "1",

doi = "10.1007/11538363\_15",

language = "English",

volume = "3634",

pages = "200--215",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

note = "19th International Workshop on Computer Science Logic, CSL 2005 and 14th Annual Conference of the EACSL ; Conference date: 22-08-2005 Through 25-08-2005",

}

TY - JOUR

T1 - Focusing the inverse method for linear logic

AU - Chaudhuri, Kaustuv

AU - Pfenning, Frank

PY - 2005/1/1

Y1 - 2005/1/1

N2 - 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.

AB - 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.

U2 - 10.1007/11538363_15

DO - 10.1007/11538363_15

M3 - Conference article

AN - SCOPUS:26944482708

SN - 0302-9743

VL - 3634

SP - 200

EP - 215

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 19th International Workshop on Computer Science Logic, CSL 2005 and 14th Annual Conference of the EACSL

Y2 - 22 August 2005 through 25 August 2005

ER -

Focusing the inverse method for linear logic

Abstract

Access to Document

Fingerprint

Cite this