Focused Proof Search for Linear Logic in the Calculus of Structures

Author Nicolas Guenot

Thumbnail PDF


  • Filesize: 346 kB
  • 10 pages

Document Identifiers

Author Details

Nicolas Guenot

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)


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.
  • Proof theory
  • focusing
  • proof search
  • deep inference
  • linear logic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads