Sequent reconstruction in LLM—A sweepline proof

Annals of Pure and Applied Logic 73 (3):277-295 (1995)
  Copy   BIBTEX

Abstract

An alternative proof is given that to each LLM proof net there corresponds at least one LLM sequent proof. The construction is inspired by the sweepline technique from computational geometry and includes a treatment of the multiplicative constants and of proof boxes

Categories

Keywords

Reprint years

DOI

10.1016/0168-0072(94)00033-y

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,168

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Algebraic aspects of cut elimination.Francesco Belardinelli, Peter Jipsen & Hiroakira Ono - 2004 - Studia Logica 77 (2):209 - 240.
A proof-search procedure for intuitionistic propositional logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
Extracting BB′IW Inhabitants of Simple Types From Proofs in the Sequent Calculus $${LT_\to^{t}}$$ L T → t for Implicational Ticket Entailment.Katalin Bimbó & J. Michael Dunn - 2014 - Logica Universalis 8 (2):141-164.
Proof-Theoretic Semantics, Self-Contradiction, and the Format of Deductive Reasoning.Peter Schroeder-Heister - 2012 - Topoi 31 (1):77-85.
Proof-theoretic modal pa-completeness I: A system-sequent metric.Paolo Gentilini - 1999 - Studia Logica 63 (1):27-48.
Bolzano’s concept of grounding against the background of normal proofs.Antje Rumberg - 2013 - Review of Symbolic Logic 6 (3):424-459.
The deduction rule and linear and near-linear proof simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Sequent calculus proof theory of intuitionistic apartness and order relations.Sara Negri - 1999 - Archive for Mathematical Logic 38 (8):521-547.
A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language.Michael Gabbay - 2011 - Journal of Symbolic Logic 76 (2):673 - 699.
Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.
Admissibility of structural rules for contraction-free systems of intuitionistic logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
Admissibility of cut in congruent modal logics.Andrzej Indrzejczak - 2011 - Logic and Logical Philosophy 20 (3):189-203.

Analytics

Added to PP
2014-01-16

Downloads
20 (#770,420)

6 months
4 (#796,773)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

No references found.

Add more references