License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICLP.2010.84
URN: urn:nbn:de:0030-drops-25868
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2586/
Go to the corresponding LIPIcs Volume Portal

Guenot, Nicolas

Focused Proof Search for Linear Logic in the Calculus of Structures

pdf-format:
10003.GuenotNicolas.2586.pdf (0.3 MB)

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.

BibTeX - Entry

@InProceedings{guenot:LIPIcs:2010:2586,
  author =	{Nicolas Guenot},
  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 =	{Manuel Hermenegildo and Torsten Schaub},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2586},
  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}
}

Keywords: Proof theory, focusing, proof search, deep inference, linear logic
Collection: Technical Communications of the 26th International Conference on Logic Programming
Issue Date: 2010
Date of publication: 25.06.2010

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