License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2011.159
URN: urn:nbn:de:0030-drops-32297
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3229/
Go to the corresponding LIPIcs Volume Portal

Chaudhuri, Kaustuv ; Guenot, Nicolas ; Straßburger, Lutz

The Focused Calculus of Structures

pdf-format:
16.pdf (1.0 MB)

Abstract

The focusing theorem identifies a complete class of sequent proofs that have no inessential non-deterministic choices and restrict the essential choices to a particular normal form. Focused proofs are therefore well suited both for the search and for the representation of sequent proofs. The calculus of structures is a proof formalism that allows rules to be applied deep inside a formula. Through this freedom it can be used to give analytic proof systems for a wider variety of logics than the sequent calculus, but standard presentations of this calculus are too permissive, allowing too many proofs. In order to make it more amenable to proof search, we transplant the focusing theorem from the sequent calculus to the calculus of structures. The key technical contribution is an incremental treatment of focusing that avoids trivializing the calculus of structures. We give a direct inductive proof of the completeness of the focused calculus of structures with respect to a more standard unfocused form. We also show that any focused sequent proof can be represented in the focused calculus of structures, and, conversely, any proof in the focused calculus of structures corresponds to a focused sequent proof.

BibTeX - Entry

@InProceedings{chaudhuri_et_al:LIPIcs:2011:3229,
  author =	{Kaustuv Chaudhuri and Nicolas Guenot and Lutz Stra{\ss}burger},
  title =	{{The Focused Calculus of Structures}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{159--173},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Marc Bezem},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3229},
  URN =		{urn:nbn:de:0030-drops-32297},
  doi =		{10.4230/LIPIcs.CSL.2011.159},
  annote =	{Keywords: focusing, polarity, calculus of structures, linear logic}
}

Keywords: focusing, polarity, calculus of structures, linear logic
Collection: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
Issue Date: 2011
Date of publication: 31.08.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI