Passer à la navigation principale Passer à la recherche Passer au contenu principal

Canonical sequent proofs via multi-focusing

  • INRIA
  • Laboratoire d'Informatique (LIX)

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collectionContribution à une conférenceRevue par des pairs

Résumé

The sequent calculus admits many proofs of the same conclusion that differ only by trivial permutations of inference rules. In order to eliminate this "bureaucracy" from sequent proofs, deductive formalisms such as proof nets or natural deduction are usually used instead of the sequent calculus, for they identify proofs more abstractly and geometrically. In this paper we recover permutative canonicity directly in the cut-free sequent calculus by generalizing focused sequent proofs to admit multiple foci, and then considering the restricted class of maximally multi-focused proofs. We validate this definition by proving a bijection to the well-known proof-nets for the unit-free multiplicative linear logic, and discuss the possibility of a similar correspondence for larger fragments.

langue originaleAnglais
titreFifth Ifip International Conference On Theoretical Computer Science - Tcs 2008
EditeurSpringer New York
Pages383-396
Nombre de pages14
ISBN (imprimé)9780387096797
Les DOIs
étatPublié - 1 janv. 2008

Série de publications

NomIFIP International Federation for Information Processing
Volume273
ISSN (imprimé)1571-5736

Empreinte digitale

Examiner les sujets de recherche de « Canonical sequent proofs via multi-focusing ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation