10 found
Order:
  1.  23
    A New Deconstructive Logic: Linear Logic.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1997 - Journal of Symbolic Logic 62 (3):755-807.
    The main concern of this paper is the design of a noetherian and confluent normalization for LK 2. The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD, delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' to classical logic ; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic using (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  2.  8
    LKQ and LKT: Sequent Calculi for Second Order Logic Based Upon Dual Linear Decompositions of Classical Implication.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1995 - In Jean-Yves Girard, Yves Lafont & Laurent Regnier (eds.), Advances in Linear Logic. Cambridge University Press. pp. 222--211.
  3.  19
    On the Linear Decoration of Intuitionistic Derivations.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1995 - Archive for Mathematical Logic 33 (6):387-412.
    We define an optimal proof-by-proof embedding of intuitionistic sequent calculus into linear logic and analyse the (purely logical) linearity information thus obtained.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  4.  10
    SN and {CR} for Free-Style {${Bf LK}Sp {Tq}$}: Linear Decorations and Simulation of Normalization.Jean-Baptiste Joinet, Harold Schellinx & Lorenzo Tortora de Falco - 2002 - Journal of Symbolic Logic 67 (1):162-196.
    The present report is a, somewhat lengthy, addendum to "A new deconstructive logic: linear logic," where the elimination of cuts from derivations in sequent calculus for classical logic was studied ‘from the point of view of linear logic’. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives.The main novelty here is the observation that this type-distinction is not essential: we can allow classical (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  18
    A Linear Approach to Modal Proof Theory.Harold Schellinx - 1996 - In H. Wansing (ed.), Proof Theory of Modal Logic. Kluwer Academic Publishers. pp. 33.
  6.  26
    Isomorphisms and Nonisomorphisms of Graph Models.Harold Schellinx - 1991 - Journal of Symbolic Logic 56 (1):227-249.
    In this paper the existence or nonexistence of isomorphic mappings between graph models for the untyped lambda calculus is studied. It is shown that Engeler's D A is completely determined, up to isomorphism, by the cardinality of its `atom-set' A. A similar characterization is given for a collection of graph models of the Pω-type; from this some propositions regarding automorphisms are obtained. Also we give an indication of the complexity of the first-order theory of graph models by showing that the (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  7.  10
    On the Jordan-Hölder Decomposition of Proof Nets.Quintijn Puite & Harold Schellinx - 1997 - Archive for Mathematical Logic 37 (1):59-65.
    Having defined a notion of homology for paired graphs, Métayer ([Ma]) proves a homological correctness criterion for proof nets, and states that for any proof net $G$ there exists a Jordan-Hölder decomposition of ${\mathsf H}_0(G)$ . This decomposition is determined by a certain enumeration of the pairs in $G$ . We correct his proof of this fact and show that there exists a 1-1 correspondence between these Jordan-Hölder decompositions of ${\mathsf H}_0(G)$ and the possible ‘construction-orders’ of the par-net underlying $G$.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  8.  19
    Basic Proof Theory, A.S. Troelstra and H. Schwichtenberg.Harold Schellinx - 1998 - Journal of Logic, Language and Information 7 (2):221-223.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  9.  2
    Preface.Jaap van Oosten & Harold Schellinx - 2002 - Annals of Pure and Applied Logic 114 (1-3):1-2.
  10. SN and CR for Free-Style LKtq: Linear Decorations and Simulation of Normalization.Jean-Baptiste Joinet, Harold Schellinx & Lorenzo Tortora De Falco - 2002 - Journal of Symbolic Logic 67 (1):162-196.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark