5 found
Order:
  1.  12
    Misao Nagayama (1999). Normalization Theorem for P-W. Bulletin of the Section of Logic 28 (2):83-88.
    Direct download  
     
    Export citation  
     
    My bibliography  
  2.  11
    Sachio Hirokawa, Yuichi Komori & Misao Nagayama (2000). A Lambda Proof of the P-W Theorem. Journal of Symbolic Logic 65 (4):1841-1849.
    The logical system P-W is an implicational non-commutative intuitionistic logic defined by axiom schemes B = (b → c) → (a → b) → a → c, B' = (a → b) → (b → c) → a → c, I = a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α = β holds if α → β and β → α are both provable in P-W. The answer is (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  3.  11
    Misao Nagayama (1994). On a Property of BCK-Identities. Studia Logica 53 (2):227 - 234.
    A BCK-algebra is an algebra in which the terms are generated by a set of variables, 1, and an arrow. We mean by aBCK-identity an equation valid in all BCK-algebras. In this paper using a syntactic method we show that for two termss andt, if neithers=1 nort=1 is a BCK-identity, ands=t is a BCK-identity, then the rightmost variables of the two terms are identical.This theorem was conjectured firstly in [5], and then in [3]. As a corollary of this theorem, we (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  4.  9
    Misao Nagayama (1992). On Boolean Algebras and Integrally Closed Commutative Regular Rings. Journal of Symbolic Logic 57 (4):1305-1318.
    In this paper we consider properties, related to model-completeness, of the theory of integrally closed commutative regular rings. We obtain the main theorem claiming that in a Boolean algebra B, the truth of a prenex Σn-formula whose parameters ai partition B, can be determined by finitely many conditions built from the first entry of Tarski invariant T(ai)'s, n-characteristic D(n, ai)'s and the quantities S(ai, l) and S'(ai, l) for $l < n$. Then we derive two important theorems. One claims that (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  5.  7
    Misao Nagayama & Mitsuhiro Okada (2001). A New Correctness Criterion for the Proof Nets of Non-Commutative Multiplicative Linear Logics. Journal of Symbolic Logic 66 (4):1524-1542.
    This paper presents a new correctness criterion for marked Danos-Reginer graphs (D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL. As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography