LIPIcs.ICLP.2010.84.pdf
- Filesize: 346 kB
- 10 pages
Document
Focused Proof Search for Linear Logic in the Calculus of Structures
Author
-
Part of:
Volume:
Technical Communications of the 26th International Conference on Logic Programming (ICLP 2010)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Logic Programming (ICLP) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2010-06-25
Cite AsGet BibTex
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)
https://doi.org/10.4230/LIPIcs.ICLP.2010.84
https://doi.org/10.4230/LIPIcs.ICLP.2010.84
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.
Keywords
- Proof theory
- focusing
- proof search
- deep inference
- linear logic
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads