Guenot, Nicolas
Focused Proof Search for Linear Logic in the Calculus of Structures
Abstract
The prooftheoretic approach to logic programming has benefited from the introduction of focused proof systems, through the nondeterminism 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 nondeterminism 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 = {8493},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897170},
ISSN = {18688969},
year = {2010},
volume = {7},
editor = {Manuel Hermenegildo and Torsten Schaub},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2010/2586},
URN = {urn:nbn:de:0030drops25868},
doi = {http://dx.doi.org/10.4230/LIPIcs.ICLP.2010.84},
annote = {Keywords: Proof theory, focusing, proof search, deep inference, linear logic}
}
2010
Keywords: 

Proof theory, focusing, proof search, deep inference, linear logic 
Seminar: 

Technical Communications of the 26th International Conference on Logic Programming

Related Scholarly Article: 


Issue date: 

2010 
Date of publication: 

2010 