5 found
Order:
  1.  6
    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)  
     
    Export citation  
     
    My bibliography   1 citation  
  2.  5
    Koji Nakazawa & Ken-Etsu Fujita (2016). Compositional Z: Confluence Proofs for Permutative Conversion. Studia Logica 104 (6):1205-1224.
    This paper gives new confluence proofs for several lambda calculi with permutation-like reduction, including lambda calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions, and a lambda calculus with explicit substitutions. For lambda calculi with permutative conversion, naïve parallel reduction technique does not work, and traditional notion of residuals is required as Ando pointed out. This paper shows that the difficulties can be avoided by extending the technique proposed by Dehornoy and van Oostrom, called the Z (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  3.  28
    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)  
     
    Export citation  
     
    My bibliography  
  4.  4
    Ken-Etsu Fujita, Ryo Kashima, Yuichi Komori & Naosuke Matsuda (2015). Reduction Rules for Intuitionistic {{Lambda}{Rho}}-Calculus. Studia Logica 103 (6):1225-1244.
    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, and give (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  5.  6
    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)  
     
    Export citation  
     
    My bibliography