4 found
Sort by:
  1. Ken-Etsu Fujita, Ryo Kashima, Yuichi Komori & Naosuke Matsuda (forthcoming). Reduction Rules for Intuitionistic {{Lambda}{Rho}}-Calculus. Studia Logica:1-20.
    The third author gave a natural deduction style proof system called the \-calculus for implicational fragment of classical logic in . In -calculus, 2015, Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues”, to appear), the fourth author gave a natural subsystem “intuitionistic \-calculus” of the \-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus , but is complicated. In this paper, we introduce some reduction rules for the \-calculus, (...)
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  2. Makoto Tatsuta, Ken-Etsu Fujita, Ryu Hasegawa & Hiroshi Nakano (2010). Inhabitation of Polymorphic and Existential Types. Annals of Pure and Applied Logic 161 (11):1390-1399.
    This paper shows that the inhabitation problem in the lambda calculus with negation, product, polymorphic, and existential types is decidable, where the inhabitation problem asks whether there exists some term that belongs to a given type. In order to do that, this paper proves the decidability of the provability in the logical system defined from the second-order natural deduction by removing implication and disjunction. This is proved by showing the quantifier elimination theorem and reducing the problem to the provability in (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  3. Ken-etsu Fujita (1998). On Proof Terms and Embeddings of Classical Substructural Logics. Studia Logica 61 (2):199-221.
    There is an intimate connection between proofs of the natural deduction systems and typed lambda calculus. It is well-known that in simply typed lambda calculus, the notion of formulae-as-types makes it possible to find fine structure of the implicational fragment of intuitionistic logic, i.e., relevant logic, BCK-logic and linear logic. In this paper, we investigate three classical substructural logics (GL, GLc, GLw) of Gentzen's sequent calculus consisting of implication and negation, which contain some of the right structural rules. In terms (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  4. Hans Tonino & Ken-Etsu Fujita (1992). On the Adequacy of Representing Higher Order Intuitionistic Logic as a Pure Type System. Annals of Pure and Applied Logic 57 (3):251-276.
    In this paper we describe the Curry-Howard-De Bruijn isomorphism between Higher Order Many Sorted Intuitionistic Predicate Logic PREDω and the type system λPREDω, which can be considered a subsystem of the Calculus of Constructions. The type system is presented using the concept of a Pure Type System, which is a very elegant framework for describing type systems. We show in great detail how formulae and proof trees of the logic relate to types and terms of the type system, respectively. Finally, (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation