Search Results

Documents authored by Guenot, Nicolas

Document
DOI: 10.4230/LIPIcs.CSL.2011.159
The Focused Calculus of Structures

Authors: Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

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.
Cite as

Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The Focused Calculus of Structures. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 159-173, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{chaudhuri_et_al:LIPIcs.CSL.2011.159,
  author =	{Chaudhuri, Kaustuv and Guenot, Nicolas and Stra{\ss}burger, Lutz},
  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 =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.159},
  URN =		{urn:nbn:de:0030-drops-32297},
  doi =		{10.4230/LIPIcs.CSL.2011.159},
  annote =	{Keywords: focusing, polarity, calculus of structures, linear logic}
}
Document
DOI: 10.4230/LIPIcs.ICLP.2010.84
Focused Proof Search for Linear Logic in the Calculus of Structures

Authors: Nicolas Guenot

Published in: LIPIcs, Volume 7, Technical Communications of the 26th International Conference on Logic Programming (2010)

Abstract
The proof-theoretic approach to logic programming has benefited from the introduction of focused proof systems, through the non-determinism reduction and control they provide when searching for proofs in the sequent calculus. However, this technique was not available in the calculus of structures, known for inducing even more non-determinism than other logical formalisms. This work in progress aims at translating the notion of focusing into the presentation of linear logic in this setting, and use some of its specific features, such as deep application of rules and fine granularity, in order to improve proof search procedures. The starting point for this research line is the multiplicative fragment of linear logic, for which a simple focused proof system can be built.
Cite as

Nicolas Guenot. Focused Proof Search for Linear Logic in the Calculus of Structures. In Technical Communications of the 26th International Conference on Logic Programming. Leibniz International Proceedings in Informatics (LIPIcs), Volume 7, pp. 84-93, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{guenot:LIPIcs.ICLP.2010.84,
  author =	{Guenot, Nicolas},
  title =	{{Focused Proof Search for Linear Logic in the Calculus of Structures}},
  booktitle =	{Technical Communications of the 26th International Conference on Logic Programming},
  pages =	{84--93},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-17-0},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{7},
  editor =	{Hermenegildo, Manuel and Schaub, Torsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2010.84},
  URN =		{urn:nbn:de:0030-drops-25868},
  doi =		{10.4230/LIPIcs.ICLP.2010.84},
  annote =	{Keywords: Proof theory, focusing, proof search, deep inference, linear logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact