## Works by Yuichi Komori

11 found
Order:
1. Hiroakira Ono & Yuichi Komori (1985). Logics Without the Contraction Rule. Journal of Symbolic Logic 50 (1):169-201.

Export citation

My bibliography   33 citations
2. Yuichi Komori, Naosuke Matsuda & Fumika Yamakawa (2014). A Simplified Proof of the Church–Rosser Theorem. Studia Logica 102 (1):175-183.
Takahashi translation * is a translation which means reducing all of the redexes in a λ-term simultaneously. In [4] and [5], Takahashi gave a simple proof of the Church–Rosser confluence theorem by using the notion of parallel reduction and Takahashi translation. Our aim of this paper is to give a simpler proof of Church–Rosser theorem using only the notion of Takahashi translation.

Export citation

My bibliography   1 citation
3. Yuichi Komori (1986). Predicate Logics Without the Structure Rules. Studia Logica 45 (4):393 - 404.
In our previous paper [5], we have studied Kripke-type semantics for propositional logics without the contraction rule. In this paper, we will extend our argument to predicate logics without the structure rules. Similarly to the propositional case, we can not carry out Henkin's construction in the predicate case. Besides, there exists a difficulty that the rules of inference () and () are not always valid in our semantics. So, we have to introduce a notion of normal models.

Export citation

My bibliography   8 citations
4. Yuichi Komori (1994). Syntactical Investigations intoBI Logic andBB′I Logic. Studia Logica 53 (3):397 - 416.
In this note, we will study four implicational logicsB, BI, BB and BBI. In [5], Martin and Meyer proved that a formula is provable inBB if and only if is provable inBBI and is not of the form of » . Though it gave a positive solution to theP - W problem, their method was semantical and not easy to grasp. We shall give a syntactical proof of the syntactical relation betweenBB andBBI logics. It also includes a syntactical proof of (...)

Export citation

My bibliography   1 citation
5. Yuichi Komori & Arato Cho (2002). 1 The Type Free Λρ-Calculus. Bulletin of the Section of Logic 31 (2):65-70.

Export citation

My bibliography
6. Sachio Hirokawa, Yuichi Komori & Izumi Takeuti (1996). A Reduction Rule for Peirce Formula. Studia Logica 56 (3):419 - 426.
A reduction rule is introduced as a transformation of proof figures in implicational classical logic. Proof figures are represented as typed terms in a -calculus with a new constant P (()). It is shown that all terms with the same type are equivalent with respect to -reduction augmented by this P-reduction rule. Hence all the proofs of the same implicational formula are equivalent. It is also shown that strong normalization fails for P-reduction. Weak normalization is shown for P-reduction with another (...)

Export citation

My bibliography   1 citation
7. 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 (...)

Export citation

My bibliography
8. Yuichi Komori (1989). Logic Based on Combinators. Bulletin of the Section of Logic 18 (3):100-104.

Export citation

My bibliography
9. 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 (...)

Export citation

My bibliography
10. Yuichi Komori (1986). A New Semantics for Intuitionistic Predicate Logic. Studia Logica 45 (1):9 - 17.
The main part of the proof of Kripke's completeness theorem for intuitionistic logic is Henkin's construction. We introduce a new Kripke-type semantics with semilattice structures for intuitionistic logic. The completeness theorem for this semantics can he proved without Henkin's construction.