9 found
Order:
  1.  31
    Algebraic Proof Theory for Substructural Logics: Cut-Elimination and Completions.Agata Ciabattoni, Nikolaos Galatos & Kazushige Terui - 2012 - Annals of Pure and Applied Logic 163 (3):266-290.
  2.  12
    Which Structural Rules Admit Cut Elimination? An Algebraic Criterion.Kazushige Terui - 2007 - Journal of Symbolic Logic 72 (3):738 - 754.
    Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics. We consider full Lambek calculus (FL), i.e., intuitionistic logic without any structural rules, (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  3.  15
    The Finite Model Property for Various Fragments of Intuitionistic Linear Logic.Mitsuhiro Okada & Kazushige Terui - 1999 - Journal of Symbolic Logic 64 (2):790-802.
    Recently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic (MALL) and for affine logic (LLW), i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL (which we call IMALL), and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model property for contractive linear logic (LLC), i.e., linear logic with contraction, and for its intuitionistic version (ILLC). (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   10 citations  
  4.  22
    Towards a Semantic Characterization of Cut-Elimination.Agata Ciabattoni & Kazushige Terui - 2006 - Studia Logica 82 (1):95-119.
    We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  5.  14
    Light Affine Set Theory: A Naive Set Theory of Polynomial Time.Kazushige Terui - 2004 - Studia Logica 77 (1):9 - 40.
    In [7], a naive set theory is introduced based on a polynomial time logical system, Light Linear Logic (LLL). Although it is reasonably claimed that the set theory inherits the intrinsically polytime character from the underlying logic LLL, the discussion there is largely informal, and a formal justification of the claim is not provided sufficiently. Moreover, the syntax is quite complicated in that it is based on a non-traditional hybrid sequent calculus which is required for formulating LLL.In this paper, we (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  6.  31
    Light Affine Lambda Calculus and Polynomial Time Strong Normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
    Light Linear Logic (LLL) and Intuitionistic Light Affine Logic (ILAL) are logics that capture polynomial time computation. It is known that every polynomial time function can be represented by a proof of these logics via the proofs-as-programs correspondence. Furthermore, there is a reduction strategy which normalizes a given proof in polynomial time. Given the latter polynomial time “weak” normalization theorem, it is natural to ask whether a “strong” form of polynomial time normalization theorem holds or not. In this paper, we (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  7.  6
    Algebraic Proof Theory: Hypersequents and Hypercompletions.Agata Ciabattoni, Nikolaos Galatos & Kazushige Terui - 2017 - Annals of Pure and Applied Logic 168 (3):693-737.
  8.  14
    Agata Ciabattoni.Kazushige Terui - 2006 - Studia Logica 82:95-119.
    No categories
    Direct download  
     
    Export citation  
     
    My bibliography  
  9. The Finite Model Property for Various Fragments of Intuitionistic Linear Logic.Mitsuhiro Okada & Kazushige Terui - 1999 - Journal of Symbolic Logic 64 (2):790-802.
    Recently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic and for affine logic, i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL, and intuitionistic LLW. In addition, we shall show the finite model property for contractive linear logic, i.e., linear logic with contraction, and for its intuitionistic version. The finite model property for related substructural logics also follow by our (...)
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography