10 found
Sort by:
  1. Jean-Baptiste Joinet, Harold Schellinx & Lorenzo Tortora de Falco (2002). SN and CR for Free-Style LKtq: Linear Decorations and Simulation of Normalization. Journal of Symbolic Logic 67 (1):162-196.
    The present report is a, somewhat lengthy, addendum to [4], 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 sequent derivations to use (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2. Jean-Baptiste Joinet, Harold Schellinx & Lorenzo Tortora de Falco (2002). SN and {CR} for Free-Style {${Bf LK}Sp {Tq}$}: Linear Decorations and Simulation of Normalization. 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 (2 more)  
     
    My bibliography  
     
    Export citation  
  3. Jaap van Oosten & Harold Schellinx (2002). Preface. Annals of Pure and Applied Logic 114 (1-3):1-2.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  4. Harold Schellinx (1998). Basic Proof Theory, A.S. Troelstra and H. Schwichtenberg. Journal of Logic, Language and Information 7 (2):221-223.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  5. Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx (1997). A New Deconstructive Logic: Linear Logic. 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 (that is, classical second order predicate logic presented as a sequent calculus). 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 ([10, 12, 32, 36]), delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' ([26, 27]) to classical logic; it (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  6. Quintijn Puite & Harold Schellinx (1997). On the Jordan-Hölder Decomposition of Proof Nets. 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$.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  7. Harold Schellinx (1996). A Linear Approach to Modal Proof Theory. In H. Wansing (ed.), Proof Theory of Modal Logic. Kluwer. 33.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  8. Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx (1995). LKQ and LKT: Sequent Calculi for Second Order Logic Based Upon Dual Linear Decompositions of Classical Implication. In Jean-Yves Girard, Yves Lafont & Laurent Regnier (eds.), Advances in Linear Logic. Cambridge University Press. 222--211.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  9. Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx (1995). On the Linear Decoration of Intuitionistic Derivations. 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.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  10. Harold Schellinx (1991). Isomorphisms and Nonisomorphisms of Graph Models. 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 (6 more)  
     
    My bibliography  
     
    Export citation