7 found
Sort by:
  1. Agata Ciabattoni, Nikolaos Galatos & Kazushige Terui (2012). Algebraic Proof Theory for Substructural Logics: Cut-Elimination and Completions. Annals of Pure and Applied Logic 163 (3):266-290.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  2. Kazushige Terui (2007). Which Structural Rules Admit Cut Elimination? An Algebraic Criterion. 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 (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Kazushige Terui (2007). Light Affine Lambda Calculus and Polynomial Time Strong Normalization. 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 (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  4. Agata Ciabattoni & Kazushige Terui (2006). Towards a Semantic Characterization of Cut-Elimination. 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)  
     
    My bibliography  
     
    Export citation  
  5. Kazushige Terui (2006). Agata Ciabattoni. Studia Logica 82:95-119.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  6. Kazushige Terui (2004). Light Affine Set Theory: A Naive Set Theory of Polynomial Time. 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)  
     
    My bibliography  
     
    Export citation  
  7. Mitsuhiro Okada & Kazushige Terui (1999). The Finite Model Property for Various Fragments of Intuitionistic Linear Logic. 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 (6 more)  
     
    My bibliography  
     
    Export citation