5 found
Order:
  1.  16
    Call-by-name reduction and cut-elimination in classical logic.Kentaro Kikuchi - 2008 - Annals of Pure and Applied Logic 153 (1-3):38-65.
    We present a version of Herbelin’s image-calculus in the call-by-name setting to study the precise correspondence between normalization and cut-elimination in classical logic. Our translation of λμ-terms into a set of terms in the calculus does not involve any administrative redexes, in particular η-expansion on μ-abstraction. The isomorphism preserves β,μ-reduction, which is simulated by a local-step cut-elimination procedure in the typed case, where the reduction system strictly follows the “ cut=redex” paradigm. We show that the underlying untyped calculus is confluent (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  2.  35
    Sequent Calculi for Visser's Propositional Logics.Kentaro Kikuchi & Ryo Kashima - 2001 - Notre Dame Journal of Formal Logic 42 (1):1-22.
    This paper introduces sequent systems for Visser's two propositional logics: Basic Propositional Logic (BPL) and Formal Propositional Logic (FPL). It is shown through semantical completeness that the cut rule is admissible in each system. The relationships with Hilbert-style axiomatizations and with other sequent formulations are discussed. The cut-elimination theorems are also demonstrated by syntactical methods.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  3.  26
    Dual-Context Sequent Calculus and Strict Implication.Kentaro Kikuchi - 2002 - Mathematical Logic Quarterly 48 (1):87-92.
    We introduce a dual-context style sequent calculus which is complete with respectto Kripke semantics where implication is interpreted as strict implication in the modal logic K. The cut-elimination theorem for this calculus is proved by a variant of Gentzen's method.
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  46
    A cut-free Gentzen formulation of basic propositional calculus.Kentaro Kikuchi & Katsumi Sasaki - 2003 - Journal of Logic, Language and Information 12 (2):213-225.
    We introduce a Gentzen style formulation of Basic Propositional Calculus(BPC), the logic that is interpreted in Kripke models similarly tointuitionistic logic except that the accessibility relation of eachmodel is not necessarily reflexive. The formulation is presented as adual-context style system, in which the left hand side of a sequent isdivided into two parts. Giving an interpretation of the sequents inKripke models, we show the soundness and completeness of the system withrespect to the class of Kripke models. The cut-elimination theorem isproved (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  5.  71
    Relationships between basic propositional calculus and substructural logics.Kentaro Kikuchi - 2001 - Bulletin of the Section of Logic 30 (1):15-20.
    Direct download  
     
    Export citation  
     
    Bookmark