Details of a Researcher - Okada, Mitsuhiro

Papers - Okada, Mitsuhiro

Division display >> ／ All the affair displays 1 - 132 of about 132

Assessing Large Language Models with NeuBAROCO: Syllogistic Reasoning Ability and Biases,

Risako Ando, Hirohiko Abe, Takanobu Morishita, Koji Mineshima, Mitsuhiro Okada

ric. NAPTURAL LOGIC MEETS MACHINE LEARNING, June, 2023 (IWCS, LOGIC MEETS MACHINE LEARNING,) 4 2023.06

Last author, Accepted

Wittgenstein’s Struggle with Intuitionism, in Wittgenstein’s Philosophy in 1929

Mathieu Marion and Mitsuhir Okada

Studies in Twentieth-Century Philosophy) H 230 (Routledge) 230 1 - 16 2023.02

Part of collection (book), Joint Work, Corresponding author

Abductive Reasoning with Syllogistic Forms in Large Language Models

Abe H., Ando R., Morishita T., Ozeki K., Mineshima K., Okada M.

Lecture Notes in Computer Science 15504 LNCS 3 - 17 2025

ISSN 03029743

Research in AI using Large-Language Models (LLMs) is rapidly evolving, and the comparison of their performance with human reasoning has become a key concern. Prior studies have indicated that LLMs and humans share similar biases, such as dismissing logically valid inferences that contradict common beliefs. However, criticizing LLMs for these biases might be unfair, considering our reasoning not only involves formal deduction but also abduction, which draws tentative conclusions from limited information. Abduction can be regarded as the inverse form of syllogism in its basic structure, that is, a process of drawing a minor premise from a major premise and conclusion. This paper explores the accuracy of LLMs in abductive reasoning by converting a syllogistic dataset into one suitable for abduction. It aims to investigate whether the state-of-the-art LLMs exhibit biases in abduction and to identify potential areas for improvement, emphasizing the importance of contextualized reasoning beyond formal deduction. This investigation is vital for advancing the understanding and application of LLMs in complex reasoning tasks, offering insights into bridging the gap between machine and human cognition.

Access to Document (DOI)

An Eye-Tracking Study on the Effects of Using Highlighted Multi-attribute Tables: A Preliminary Report

Morii M., Ideno T., Tamari Y., Takemura K., Okada M.

Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics 14981 LNAI 467 - 471 2024

ISSN 03029743

Our previous research, aimed at improving the design of multi-attribute tables (such as product catalogs), found that black-and-white graphics aided decision-making more than numerical or textual formats (Ideno et al., Diagrams 2020). We extended these findings by examining how combining graphic and numerical presentation (highlighting the cells with superior values) influences decision-making. Twenty-one participants chose the most desirable digital cameras from five alternatives. Results showed faster decision-making with highlighted cells compared to non-highlighted ones. A two-stage decision strategy emerged, with more attribute-based gaze shifts initially and equal vertical and horizontal shifts later. We discussed the implications and prospects of highlighted multi-attribute tables.

Access to Document (DOI)

Can Euler Diagrams Improve Syllogistic Reasoning in Large Language Models?

Ando R., Ozeki K., Morishita T., Abe H., Mineshima K., Okada M.

Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics 14981 LNAI 232 - 248 2024

ISSN 03029743

In recent years, research on large language models (LLMs) has been advancing rapidly, making the evaluation of their reasoning abilities a crucial issue. Within cognitive science, there has been extensive research on human reasoning biases. It is widely observed that humans often use graphical representations as auxiliary tools during inference processes to avoid reasoning biases. However, currently, the evaluation of LLMs’ reasoning abilities has largely focused on linguistic inferences, with insufficient attention given to inferences using diagrams. In this study, we concentrate on syllogisms, a basic form of logical reasoning, and evaluate the reasoning abilities of LLMs supplemented by Euler diagrams. We systematically investigate how accurately LLMs can perform logical reasoning when using diagrams as auxiliary input and whether they exhibit similar reasoning biases to those of humans. Our findings indicate that, overall, providing diagrams as auxiliary input tends to improve models’ performance, including in problems that show reasoning biases, but the effect varies depending on the conditions, and the improvement in accuracy is not as high as that seen in humans. We present results from experiments conducted under multiple conditions, including a Chain-of-Thought setting, to highlight where there is room to improve logical diagrammatic reasoning abilities of LLMs.

Access to Document (DOI)

Exploring Reasoning Biases in Large Language Models Through Syllogism: Insights from the NeuBAROCO Dataset

Ozeki K., Ando R., Morishita T., Abe H., Mineshima K., Okada M.

Proceedings of the Annual Meeting of the Association for Computational Linguistics 16063 - 16077 2024

ISSN 0736587X

This paper explores the question of how accurately current large language models can perform logical reasoning in natural language, with an emphasis on whether these models exhibit reasoning biases similar to humans. Specifically, our study focuses on syllogistic reasoning, a form of deductive reasoning extensively studied in cognitive science as a natural form of human reasoning. We present a syllogism dataset called NeuBAROCO, which consists of syllogistic reasoning problems in English and Japanese. This dataset was originally designed for psychological experiments to assess human reasoning capabilities using various forms of syllogisms. Our experiments with leading large language models indicate that these models exhibit reasoning biases similar to humans, along with other error tendencies. Notably, there is significant room for improvement in reasoning problems where the relationship between premises and hypotheses is neither entailment nor contradiction. We also present experimental results and in-depth analysis using a new Chain-of-Thought prompting method, which asks LLMs to translate syllogisms into abstract logical expressions and then explain their reasoning process. Our analysis using this method suggests that the primary limitations of LLMs lie in the reasoning process itself rather than the interpretation of syllogisms.

Access to Document (DOI)

Evaluating Large Language Models with NeuBAROCO: Syllogistic Reasoning Ability and Human-like Biases

Ando R., Morishita T., Abe H., Mineshima K., Okada M.

Iwcs2023 Proceedings of the 4th Natural Logic Meets Machine Learning Workshop Naloma 2023 1 - 11 2023

This paper investigates whether current large language models exhibit biases in logical reasoning, similar to humans. Specifically, we focus on syllogistic reasoning, a well-studied form of inference in the cognitive science of human deduction. To facilitate our analysis, we introduce a dataset called NeuBAROCO, originally designed for psychological experiments that assess human logical abilities in syllogistic reasoning. The dataset consists of syllogistic inferences in both English and Japanese. We examine three types of biases observed in human syllogistic reasoning: belief biases, conversion errors, and atmosphere effects. Our findings demonstrate that current large language models struggle more with problems involving these three types of biases.

A Semantics for “Typically” in First-Order Default Reasoning

Bana G., Okada M.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)) 12758 LNAI 3 - 20 2021

ISSN 03029743

We present a new semantics for first-order conditional logic, which is a generalization of that of Friedman, Halpern and Koller [7]. We utilize Fitting’s embedding of first-order classical logic in first-order S4 to define our semantics. We explain our semantics by showing how it works on the connective expressing “typically implies”. We argue that it has a number of good properties, in particular, it is more adjustable to special situations than that of [7]. For example, we can make sense of nested conditional implications even when a conditional implication does not necessarily hold on the entire set of possible worlds, but where-ever it is satisfied, the conclusion is typically satisfied.

Access to Document (DOI)

A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems

Okada M., Takahashi Y.

ISSN 9783030635947

There have been some important methods of combining a recursive path ordering and Tait-Girard’s computability argument to provide an ordering for termination proofs of higher-order rewrite systems. The higher-order recursive path ordering HORPO by Jouannaud and Rubio and the computability path ordering CPO by Blanqui, Jouannaud and Rubio are examples of such an ordering. In this paper, we give a case study of yet another direction of such extension of recursive path ordering, avoiding Tait-Girard’s computability method plugged in the above mentioned works. This motivation comes from Lévy’s question in the RTA open problem 19, which asks for a reasonably straightforward interpretation of simply typed λ -calculus λ in a certain well founded ordering. As in the cases of HORPO and CPO, the addition of λ -abstraction and application into path orderings might be considered as one solution, but the following question still remains; can the termination of λ be proved by an interpretation in a first-order well founded ordering in the sense that λ -abstraction/application are not directly built in the ordering? Reconsidering one of Howard’s works on proof-theoretic studies, we introduce the path ordering with Howard algebra as a case study towards further studies on Lévy’s question. → →

Access to Document (DOI)

On Effects of Changing Multi-attribute Table Design on Decision Making: An Eye-Tracking Study

Ideno T., Morii M., Takemura K., Okada M.

ISSN 9783030542481

Information tables are often used for decision making. This study considers multi-attribute table designs from a diagrammatic perspective. We used two experiments to show how the decision-making strategies and performance are changed based on table design changes, using the eye-tracking method. We employed a multi-attribute catalog table with alternatives presented along the horizontal axis and attributes along the vertical axis in Experiment 1 and the opposite layout in Experiment 2. In each experiment, we used four different types of representations of the attribute values, and these values were restricted to two levels for comparison with previous works. The four types used were: (i) numerical representations, (ii) textual representations, (iii) black-and-white representations with black representing better values, and (iv) black-and-while representations with white representing better values. Our results suggest, among others, that (1) placing the alternatives along the vertical axis makes the table easier to decide in comparison to the opposite layout, and that (2) the two-stage decision strategy is taken with numerical representations and textual representations, while a single stage strategy is taken with the black-and-white representations. We also showed how the graphic black-and-white representations made decision-making easier, and how the order changes of alternatives and of attributes of a table influenced decision makers’ decision.

Access to Document (DOI)

A Small Remark on Hilbert’s Finitist View of Divisibility and Kanovich-Okada-Scedrov’s Logical Analysis of Real-Time Systems

Okada M.

ISSN 03029743

Hilbert remarked in the introductory part of his most famous finitism address (1925 [1]) that “[t]he infinite divisibility of a continuum is an operation that is present only in our thought”, which means that no natural event or matter is infinitely divisible in reality. We recall that Scedrov’s group including the author started logical analysis of real time systems with the principle similar to Hilbert’s no-infinite divisibility claim, in [2]. The author would like to note some early history of the group’s work on logical analysis of real time system as well as some remark related to Hilbert’s claim of no-infinite divisibility.

Access to Document (DOI)

Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability

GERGEI BANA, ROHIT CHADHA, AJAY KUMAR EERALLA, MITSUHIRO OKADA

ACM Trans. Comput. Logic (Association for Computing Machinery) to appear ( 1 ) 2019.12

Research paper (scientific journal), Accepted, ISSN 15293785

© 2019 Copyright held by the owner/author(s). In recent years, a new approach has been developed for verifying security protocols with the aim of combining the benefits of symbolic attackers and the benefits of unconditional soundness: the technique of the computationally complete symbolic attacker of Bana and Comon (BC) [8]. In this article, we argue that the real breakthrough of this technique is the recent introduction of its version for indistinguishability [9], because, with the extensions we introduce here, for the first time, there is a computationally sound symbolic technique that is syntactically strikingly simple, to which translating standard computational security notions is a straightforward matter, and that can be effectively used for verification of not only equivalence properties but trace properties of protocols as well. We first fully develop the core elements of this newer version by introducing several new axioms. We illustrate the power and the diverse use of the introduced axioms on simple examples first. We introduce an axiom expressing the Decisional Diffie-Hellman property. We analyze the Diffie-Hellman key exchange, both in its simplest form and an authenticated version as well. We provide computationally sound verification of real-or-random secrecy of the Diffie-Hellman key exchange protocol formultiple sessions, without any restrictions on the computational implementation other than the DDH assumption. We also show authentication for a simplified version of the station-to-station protocol using UF-CMA assumption for digital signatures. Finally, we axiomatize IND-CPA, IND-CCA1, and IND-CCA2 security properties and illustrate their usage. We have formalized the axiomatic system in an interactive theorem prover, Coq, and have machine-checked the proofs of various auxiliary theorems and security properties of Diffie-Hellman and station-to-station protocol.

Access to Document (DOI)

Psychosocial Twin Cohort Studies in Japan: The Keio Twin Research Center (KoTReC)

Ando J., Fujisawa K.K., Hiraishi K., Shikishima C., Kawamoto T., Nozaki M., Yamagata S., Takahashi Y., Suzuki K., Someya Y., Ozaki K., Deno M., Tanaka M., Sasaki S., Toda T., Kobayashi K., Sakagami M., Okada M., Kijima N., Takizawa R., Murayama K.

Twin Research and Human Genetics (Twin Research and Human Genetics) 22 ( 6 ) 591 - 596 2019.12

ISSN 18324274

© The Author(s) 2020. The Keio Twin Research Center (KoTReC) was established in 2009 at Keio University to combine two longitudinal cohort projects - the Keio Twin Study (KTS) for adolescence and adulthood and the Tokyo Twin Cohort Project (ToTCoP) for infancy and childhood. KoTReC also conducted a two-time panel study of self-control and psychopathology in twin adolescence in 2012 and 2013 and three independent anonymous cross-sectional twin surveys (ToTcross) before 2012 - the ToTCross, the Junior and Senior High School Survey and the High School Survey. This article introduces the recent research designs of KoTReC and its publications.

Access to Document (DOI)

On quasi-ordinal diagrams

Mitsuhiro Okada and Yuta Takahashi

38-49, EPTCS 288, Post-Workshop Proceedings of the 10th EOTCS Post-Proceedings of Workshop on Computation with Terms and Graphs (TermGraph 2018) (FEPTCS) 38 - 49 2019.03

Research paper (international conference proceedings), Joint Work, Accepted

Following a Rule: Waismann's Version

<UMarion Mathieu and Okada, Mitsuhiro(/)-#HR

Publications of the Austrian Ludwig Wittgenstein Society – New Series (Austrian Ludwig Wittgenstein Society) 2019

Research paper (international conference proceedings), Joint Work

On quasi ordinal diagram systems

Okada M., Takahashi Y.

Electronic Proceedings in Theoretical Computer Science, EPTCS (Electronic Proceedings in Theoretical Computer Science, EPTCS) 288 38 - 49 2019

ISSN 20752180

© M. Okada & Y. Takahashi. The purposes of this note are the following two; we first generalize Okada-Takeuti’s well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret’s version of tree embedding theorem with gap conditions. Second, we discuss possible use of such strong ordinal notation systems for the purpose of a typical traditional termination proof method for term rewriting systems, especially for second-order (pattern-matching-based) rewriting systems including a rewrite-theoretic version of Buchholz’s hydra game.

Access to Document (DOI)

Qualitatively coherent representation makes decision-making easier with binary-colored multi-attribute tables: An eye-tracking study

Okada, M., Morii, M., Ideno, T., Takemura, K. & Okada, M

Frontiers in Psychology (Frontiers) 8(AUG), [1388]. 2017.08

Research paper (scientific journal), Joint Work, Accepted

Access to Document (DOI)

What is logic?

Mitsuhiro Okada

Proceedings of "Beyond Logic" cericy Meeting May 21-May 26, 2017 (Cersy) 2017.07

Research paper (international conference proceedings), Single Work

Semantics for “Enough-Certainty" and Fitting’s Embedding of Classical Logic in S4

Gergei Bana and Mitsuhiro Okada

LIPIcs, Leibniz International Proceeding Series (LIPIcs, Leibniz International Proceeding Series) 34(2016) ( article 23 ) 1 - 17 2016.08

Research paper (international conference proceedings), Accepted

Access to Document (DOI)

Syntactic Reduction in Husserl's early Phenomenology of Arithmetic

Mirja Hartimo and Mitsuhiro Okada

Synthese (Springer) 193 ( 3 ) 937 - 969 2016.03

Research paper (scientific journal), Joint Work, Accepted

Access to Document (DOI)

On definite manifolds and universal arithmetic in the early Husserl: 1901 winter manuscripts

岡田光弘

Phenomenology Association of Japan (Phenomenology Association of Japan) 31 1 - 15 2015.11

Research paper (scientific journal), Single Work

Genetic Factors of Individual Differences in Decision Making in Economic Behavior: A Japanese Twin Study using the Allais Problem

Chizuru Shikishima, Kai Hiraishi, Shinji Yamagata, Juko Ando and Mitsuhiro Okada

Frontiers in Psychology, (Frontiers) 6:1712, 2015 2015

Research paper (scientific journal), Joint Work, Accepted

Access to Document (DOI)

Towards explaining the cognitive efficacy of Euler diagrams in syllogistic reasoning:A relational perspective

Mineshima,K., Sato,Y., Takemura,R., & Okada,M.

Journal of Visual Language and Computing,Vol.25,Issue 3 156 - 169 2014.06

Research paper (scientific journal), Joint Work, Accepted

Wittgenstein on Equinumerosity and Surveyability

M. Marion and M. Okada

Grazer Philosophische Studien, vol.89 89 59 - 76 2014

Research paper (scientific journal), Joint Work, Accepted

Computational Soundress of cryptographic communication protocols,CCS 2013,ACM Proceedings,Des 2013

Gergery Bana, Koji Hasebe and Mitsuhiro Okada

Association for Computing Machinery 2013.12

Research paper (international conference proceedings), Joint Work, Accepted

Computationally Complete Symbolic Attacker and Key Exchange

Gergei Bana, Koji Hasebe, Mitsuhiro Okada

SIGSAC conference on Computer and communications security (ACM) ( CCS2013 ) 1231 - 1246 2013.11

Research paper (international conference proceedings), Joint Work

Wittgenstein on Contradiction and Consistency:An Overview

Marion,M.& Okada,M.

Ludovic Soutif,tif,Luiz Carlos Pereira & Camila Jourdan(eds.)Wittgenstein:Matematica,Linguagem,Percepcao,O que nos faz pensar,n 33 50 - 79 2013.06

Research paper (scientific journal), Joint Work

Two cohort and three independent anonymous twin projects at the Keio Twin Research center(KoTReC)

Ando,J.,Hujisawa,K.,et al.(Okada,M 15/26番目）

Twin research and human genetics,Feb 2013,Vol.16,Special Issue 01 202 - 216 2013.02

Research paper (scientific journal), Joint Work

Husserl and Hilbert on Completeness and Husserl's Rewrite-Based Theory of Multiplicity

Mitsuhiro Okada

Rewrite Theory and its Applications (RTA 2013),Leibniz Internathinal Proceedings in Infomations(LIPIcs),Vol.21 (Schloss Dagtuhl-Dagstuhl Publishing) 4 - 19 2013

Research paper (international conference proceedings), Single Work

Shape Perception in Chemistry

Janna Hastings, Colin Batchelor and Mitsuhiro Okada

CEUR Proceedings 2013

Research paper (international conference proceedings), Joint Work, Accepted

On the Cognitive Efficacy of Euler Diagrams in Syllogistic Reasoning: A Relational Perspective

Yuri Sato, Koji Mineshima, Ryo Takemura, Mitsuhiro Okada

Proceedings of 3rd International Workshop on Euler Diagrams,CEUR Workshop Proceedings,Vol.854 17 - 31 2012

Research paper (international conference proceedings), Joint Work, Accepted

A Generalized Syllogistic Inference System based on Inclusion and Exclusion Relations

Koji Mineshima, Mitsuhiro Okada and Ryo Takemura

Studia Logica,Vol.100,Issue 4(Special issue,Logic and Natural Language) 100 ( 4 ) 753 - 785 2012

Research paper (scientific journal), Joint Work, Accepted

Wittgenstein et le lien entre la signification d' un enonce mathematique et sa preuve

Mathieu Marion and Mitsuhiro Okada

Philosophiques,Vol.39,n゜(Wittgenstein Special Issue) 101 - 124 2012

Research paper (scientific journal), Joint Work

A Diagrammatic Inference System with Euler Circles

Koji Mineshima, Mitsuhiro Okada and Ryo Takemura

Journal of Logic, Language and Information, Vol.21, Issue 3 365 - 391 2012

Research paper (scientific journal), Joint Work, Accepted

On The Cognitive Efficacy of Euler Diagrams in Syllogistic Reasoning: A Relational Perspective

Koji Mineshima, Yuri Sato, Ryo Takemura, and Mitsuhiro Okada.

In Proceedings of the 3rd international workshop on euler diagrams (euler diagrams 2012), CEUR Workshop Proceedings 854 17 - 31 2012

Research paper (international conference proceedings), Joint Work, Accepted

図形を用いた演繹的推論の認知プロセス

佐藤有理, 峯島宏次, 竹村亮, and 岡田光弘

日本認知科学会第28回大会論文集 269 - 274 2011

Research paper (other academic), Joint Work

Effects of aging on hemispheric asymmetry in inferior frontal cortex activity during belief-bias syllogistic reasoning: A near-infrared spectroscopy study

Takeo Tsujii, Mitsuhiro Okada, Shigeru WatanabeOKADA

Behavioural Brain Research (Behavioural Brain Research) 6 178 - 183 2010.07

オントロジーの論理学的、哲学的源泉

岡田光弘

日本人工知能学会誌　No.5 2010

Research paper (scientific journal), Single Work

オイラー図・ヴェン図を用いた図形推論の証論的分析

竹村亮、峯村宏次、佐藤有理、岡田光弘

2010年度人工知能学会全国大会(第24回）JSAI2010論文集 2010

Research paper (other academic), Joint Work

Two Types of Diagrammatic Inference System:Relation-based System as Natural Deduction and Region-based System as Resolution,2010,Proceedings of 6th International Conference on the Theory and Application of Diagrams(DIAGRAMS 2010)

Koji Mineshima,Mitsuhiro Okada and Ryo Takemura

Springer 2010

Research paper (scientific journal), Joint Work, Accepted

セキュリティプロトコルの論理的検証法

長谷部浩二、バナ・ゲルゲイ、岡田光弘

荻谷昌巳・塚田恭章共編『数理的技法による情報セキュリティ』 (共立出版) 2010

Research paper (scientific journal), Joint Work, Accepted

Secrecy-Oriented First-Order Logical Analysis of Cryptographic Protocols

Gergei Bana, Koji Hasebe, and Mitsuhiro Okada

IACR Cryptology ePrint Archive 2010

Research paper (other academic), Joint Work

Conservativity for a hierarchy of Euler and Venn reasoning systems

Koji Mineshima, Mitshihiro Okada and Ryo Takemura

Proceedings of Visual Language and Logoc 2009.,CEUR Series Vol.510 37 - 61 2009

Research paper (international conference proceedings), Joint Work, Accepted

Computational Semantics for First-Order Logical Analysis of Cryptographic protocols,Formal to Pratical Sucurity

G.Bana, K.Hasebe, M.Okada

Volume 5458 of Springer Lecture Notes in Computer Science 33 - 56 2009

Research paper (scientific journal), Joint Work, Accepted

Is g an entity? A japanese twin study using syllogysms and intelligence tests.

Chizuru Shikishima, Kai Hiraishi, Shinji Yamagata, Yutaro Sugimoto, Ryo Takemura, Koken Ozaki, Mitsuhiro Okada, Tatsushi Toda, Juko Ando

Intelligence 37 ( 3 ) 256 - 267 2009

Research paper (scientific journal), Joint Work, Accepted

Some remarks on difference between Gentzen's finitist and Heyting's intuitionist approaches toward intuitionistic logic and arithmetic.

Mitsuhiro Okada

Annals of the Japan Association for Philosophy of Science, Vol.16 1 - 18 2008

Research paper (scientific journal), Single Work, Accepted

Diagrammatic Reasoning System with Euler Circles

Koji Mineshima, Mitsuhiro Okada, Yuri Sato and Ryo takemura

Theory and Experiment Design,2008,Proceedings of 5th International Conference on the Theory and Application of Diagrams(DIAGRAMS 2008),Lecture Notes In Artificial Intelligence,Vol.5223,Springer-Verlag,188-2 2008

Research paper (scientific journal), Joint Work, Accepted

フッサール、ゲーデルから線形論理へ.

岡田光弘

「現代思想」Vol.35, No.3 149 - 163 2007.02

Research paper (scientific journal), Single Work

A proof-theoretic study of the correspondence of hybrid logic and classical logic.

HIirohiko Kushida and Mitsuhiro Okada

Journal of Logic, Language and Information, Vol.16, No.1 35 - 61 2007

Research paper (scientific journal), Joint Work, Accepted

Remarks on Semantic Completeness for Proof-Terms with Laird's Dual Affine/Intuitionistic λ-Calculus

Mitsuhiro Okada and Ryo Takemura

Volume 4600 of Lecture Notes in Computer Science, Springer 167 - 181 2007

Research paper (scientific journal), Joint Work, Accepted

Compuational Sematics for Basic Protocol Logic-A Stochastic Approach, Proceedings of ASIAN 07 the 12th Annual Asian Computing Science Conference

G.Bana, K.Hasebe and M.Okada

Vol.4846 of Lecture Notes in Compuer Science 86 - 94 2007

Research paper (scientific journal), Joint Work, Accepted

BAN論理からprotocol composition logicへ：セキュリティプロトコルの老理的検証法

長谷部浩二、岡田光弘.

応用数理、Vol.17,No.4 311 - 322 2007

Research paper (scientific journal), Joint Work, Accepted

Intuithionistic phase semantics is almost classical.

Max I.Kanovich, Mitsuhiro Okada, and Kzushige Terui

Mathematical Structures in Computer Science, Vol.16, No.1 67 - 86 2006

Research paper (scientific journal), Joint Work, Accepted

Completeness and Counter-Example Generations of a Basic Protocol Logic (extended abstract)

Mitsuhiro Okada, Koji Hasebe

6th International Workshop on Rule-Based Programming (RULE'05), volume 147 of Electronic Notes in Theoretical Computer Science to appear 73 - 92 2006

Research paper (international conference proceedings), Joint Work, Accepted

Honesty Inferences for Proving Correctness of Security Protocols

Mitsuhiro Okada and Kouji Hasebe

Workshop on New Approaches to Software Construction (WNASC 2004) 45-57 2004.09

Research paper (international conference proceedings), Joint Work, Accepted

Non-monotonic Properties for Proving Correctness in a Framework of Compositional Logic

Mitsuhiro Okada and Kouji Hasebe

Workshop on Foundations of Computer Security (FCS'04) 97-113 2004.07

Research paper (international conference proceedings), Joint Work, Accepted

Inferences on Honesty in Compositional Logic for Security Analysis

Mitsuhiro Okada and Kouji Hasebe

the International Symposium on Software Security 2003 (ISSS2003) 65-86 2004.06

Research paper (international conference proceedings), Joint Work, Accepted, ISSN 0302-9743

「矛盾は矛盾か」日本科学哲学会ラッセルパラドクス１００年特集

岡田光弘

科学哲学 36 ( 2 ) 79-102 2004

Research paper (scientific journal), Single Work, Accepted

Linear Logic and Intuitionistic Logic

Mitsuhiro Okada

La revue International de philosphie ( 230 ) 449-481 2004

Research paper (scientific journal), Single Work, Accepted

Formal Verification of Dynamic Real-Time State-Transition Systems Using Linear Logic

Koji Hasebe, Jean-Pierre Jouannaud, Antonie Kremer, Mitsuhiro Okada, and Roland Zumkeller

日本ソフトウェア科学会第20回全国大会予稿集 2003.09

Research paper (other academic), Joint Work

A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic

Mitsuhiro Okada

Theoretical Computer Science 294 ( 3 ) 551 - 573 2003.02

Research paper (scientific journal), Joint Work, Accepted

Linear Logic

J.-Y. Girard, M. Okada, A. Scedrov (guest editors)

Theoretical Computer Science 294 ( 3 ) 2003.02

Research paper (scientific journal), Single Work, Accepted

Preface

Jean-Yves Girard, Mitsuhiro Okada, and Andre Scedrov.

Theoretical Computer Science 294 ( 3 ) 2003

Research paper (scientific journal), Joint Work

Phase Semantics for Light Linear Logic

M. Konovitch, A. Scedrov, Mitsuhiro Okada

Thoretical Computer Science 294 525-549 2003

Research paper (scientific journal), Joint Work, Accepted

A Graph-Theoretic Characterization for Proofs Nets of the Multiplicative Fragment of Non-Commutative Linear Logic

N. Nagayama, Mitsuhiro Okada

Theoretical Computer Science 294 ( 3 ) 551-573 2003

Research paper (scientific journal), Joint Work, Accepted

A proof-theoretic study of the correspondence of classical logic and modal logic

M. Okada, H. Kushida

Journal of Symbolic Logic 68 ( 4 ) 1403-1414 2003

Research paper (scientific journal), Single Work, Accepted

オントロジー応用のための方法論の考察と展望

岡田光弘

人工知能学会誌 17 ( 5 ) 604-613 2002.09

Research paper (scientific journal), Single Work

現代のフォーマルオントロジーの動向とオントロジー工学

岡田光弘

人工知能学会誌 17 ( 4 ) 434-442 2002.07

Research paper (scientific journal), Single Work

A Uniform Semantic Proof for Cut-Elimination and Completeness of Various First and Higher Order Logics

Mitsuhiro Okada

Theoretical Computer Science 2002 ( 281 ) 471 - 498 2002.06

Research paper (scientific journal), Single Work, Accepted

フッサールのフォーマルオントロジーとその影響

岡田光弘

人工知能学会誌 Vol.17 ( No.3 ) 335-344 2002.05

Research paper (scientific journal), Single Work, Accepted

レクチャーシリーズ「哲学とAIにおける対象世界モデリング」の企画にあたって.

溝口理一郎, 岡田光弘.

人工知能学会誌 17 ( 2 ) 224 - 231 2002.03

Research paper (scientific journal), Joint Work

オントロジーの哲学的・論理学的背景

岡田光弘

人工知能学会誌 Vol.17 ( No.2 ) 224-231 2002.03

Research paper (scientific journal), Single Work, Accepted

Preface

Mariangiola Dezani-Ciancaglini, Mitsuhiro Okada, and Masako Takahashi.

Theoretical Computer Science 272 ( 1--2 ) 1 - 2 2002.02

Research paper (scientific journal), Joint Work, Accepted

線形論理に基づいたセキュリティ・プロトコルの論理的検証法

岡田光弘, 長谷部浩二

電子情報通信学会「人工知能と知識処理」研究会報告集 102 ( 91 ) 49 - 54 2002

Research paper (other academic), Joint Work

Inductive Date Type Systems

F. Blanqui, J-P. Jouannaud, M. Okada

Thoretical Computer Science 272 41-68 2002

Research paper (scientific journal), Joint Work, Accepted

A New Correctness Criterion for the Proof Nets of Non-Commutative Multiplicative Linear Logics

Misao Nagayama and Mitsuhiro Okada

Journal of Symbolic Logic 66 ( 4 ) 1524 - 1542 2001.12

Research paper (scientific journal), Joint Work, Accepted

A Note on Rewriting Theory for Uniqueness of Itaration

M. Okada, P-J. Scott

Theory and Applications of Categories Vol.6, No.4 Vol.6 ( No.4 ) 47-64 1999.12

Research paper (scientific journal), Joint Work, Accepted

Phase Semantic Cut-Elimination and Normalization Proofs of First- and Higher-Order Linear Logic

Mitsuhiro Okada

Theoretical Computer Science (欧州理論情報学会誌) 227 ( 1--2 ) 333 - 396 1999.09

Research paper (scientific journal), Single Work, Accepted

The Calculus of Algebraic Constructions. In Rewriting Techniques and Applications (eds. by Paliath Narendran and Michaël Rusinowitch)

Mitsuhiro Okada

Rewriting Techniques and Applications, 10th International Conference, RTA-99 Trento, Italy, July 2--4, 1999 Proceedings, volume 1631 of Lecture Notes in Computer Science 301 - 316 1999.06

Research paper (scientific journal), Single Work, Accepted

The Finite Model Property for Various Fragments of Intuitionistic Linear Logic

M. Okada, K. Terui

Journal of Symbolic Logic 64 790 - 802 1999.03

Research paper (scientific journal), Joint Work, Accepted

Specifying Real-Time Finite State Systems by Linear Logic

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov

Electoronic Notes of Theoretical Computer Science (Elsevier Science Publishing, 欧州理論情報学会編）Vol.16 Part I 1998.09

Research paper (international conference proceedings), Joint Work, Accepted

A Direct Independence Proof of Buchholz's Hydra Game on Finite Labeled Trees.

M. Hamano and M. Okada

Archive for Mathematical Logic 37 ( 2 ) 67 - 89 1998

Research paper (scientific journal), Joint Work, Accepted

Completeness Proofs for Linear Logic Based on the Proof Search Method (Preliminary Report). In RIMS Kokyuroku 1023: Type Theory and Its Applications to Computer Systems (ed. by J. Garrigue)

Mitsuhiro Okada and Kazushige Terui.

RIMS Kokyuroku 1023: Type Theory and Its Applications to Computer Systems (Research Institute for Mathematical Sciences, Kyoto University.) 57 - 75 1998

Research paper (other academic), Joint Work

Abstract Data Type Systems

J.-P. Jouannaud, M. Okada

Theoretical Computer science 173 (欧州理論情報学会誌）, 349-391 1997.12

Research paper (scientific journal), Joint Work, Accepted

Phase Semantics for Light Linear Logic (extended abstract)

M. Kanovitch, M. Okada, A. Scedrov

Electoronic Notes of Theoretical Computer Science 5(Elsevier Science Publishing, 欧州理論情報学会編） 221 - 234 1997.04

Research paper (international conference proceedings), Joint Work, Accepted

A Relationship Among Gentzen's Proof Reduction, Kirby-Paris' Hydra Game

M,Hamano, M. Okada

Mathematical Logic Quarterly 43 103-120 1997.03

Research paper (scientific journal), Joint Work, Accepted

A Hierarchy of the Fragments of the System of Inductive Definition : Preliminary Report

Masahiro Hamano and Mitsuhiro Okada

RIMS Kokyuroku 976: Proceedings of the Symposium on Proof Theory and Ordinals, edited by Toshiyasu Arai. (Research Institute for Mathematical Sciences, Kyoto University) 169 - 181 1997.02

Research paper (other academic), Joint Work

Semantic Characterizations for Reachability and Trace Equivalence in a Linear Logic-Based Process Calculus: Preliminary Report.

Mitsuhiro Okada and Kazushige Terui.

RIMS Kokyuroku 976: Proceedings of the Symposium on Proof Theory and Ordinals, edited by Toshiyasu Arai. (Research Institute for Mathematical Sciences, Kyoto University) 146 - 168 1997.02

Research paper (other academic), Joint Work

フッサールの形式論理学分析における「多様体」概念の役割

岡田光弘

哲學　三田哲学会編 ( 101 ) 1 - 43 1997

Research paper (scientific journal), Single Work

デカルトにおける「論証」の概念と彼の形而上学的論証の論理的基準

哲学　三田哲学会編 ( 第100号 ) 63-86 1996.10

Research paper (scientific journal), Single Work

Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic

Misao Nagayama and Mitsuhiro Okada

Electoronic Notes of Theoretical Computer Science 3(Elsevier Science Publishing, 欧州理論情報学会編） 1996.04

Research paper (scientific journal), Joint Work, Accepted

線形論理に基づく並行計算モデル：並行計算の論理的理解の試み

情報処理（日本情報処理学会誌）,並行計算特集 327-332 1996.04

Research paper (scientific journal), Single Work

A Higher Order Phase Semantics and Completeness, Cut-Elimination and Strong Normalization Proofs

Mitsuhiro Okada

Electoronic Notes of Theoretical Computer Science 3(Elsevier Science Publishing　欧州理論情報学会編） 1996.04

Research paper (scientific journal), Single Work, Accepted

Characterization Theorem for Multiplicative Fragment of Non-Communitative Linear Logic(Extended Abstract)

M,Nagasawa, M. Okada

Proceedings of Symposium on Kripke Models and Non-Standard Logic, Kyoto(京都大学数理解析研究所） 1995.06

Research paper (international conference proceedings), Joint Work

A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic (Preliminary Report)(Non-Classical Logics and Their Kripke Semantics)

Misao Nagayama and Mitsuhiro Okada

RIMS Kokyuroku 927: Proceedings of Symposium on Kripke Models and Non-Standard Logic (Research Institute for Mathematical Sciences, Kyoto University) 66 - 87 1995

Research paper (other academic)

人文科学の夢として、対象として,道具としてのコンピュータ

岡田光弘

三色旗　慶應義塾大学通信教育部 1994.06

Single Work

論理、言語、情報、研究余滴

岡田光弘

三田評論 1994.04

Single Work

Gentzen's Proof of Reduction, Kirby-Paris Hydra Game and Buchholz's Hydra Game

Masahiro Hamano and Mitsuhiro Okada

Proc. Of Imcomleteness in Arithmetic Symposium, Kyoto 1994 Dec.(「算術諸体系の不完全性の研究」シンポジウム）京都大学数理解析研究所講究録 64-81 1994.04

Research paper (other academic), Joint Work

A Note on the Strong Normalizability of the Self-Referential Logic

Mitsuhiro Okada

三田哲学会編　哲学第95巻 1-14 1993.12

Research paper (scientific journal), Single Work

LAMBDALG-Higher Order Algebraic Specification Language

Y.Gui, M. Okada

Proc., of Rewriting Techniques and Applications, Springer LNCS 690(ドイツSpringer社） 462-466 1993.06

Research paper (scientific journal), Joint Work, Accepted

教育と社会

岡田光弘

三色旗　慶應義塾大学通信教育部 1993.05

Single Work

Denotational Semantical Analysis on Japanese Case Particles

M. Okada, K. Watanabe

Information and Computation（Formal　GrammerTheory Series3), ed. Lee. Thaehakusa社, Seoul 145-157 1993.03

Research paper (scientific journal), Joint Work, Accepted

Rewriting Theory for the Uniqueness Condition of Higher Types

M. Okada, P.J. Scott

Proc. Of the　Montreal Workshop on Programing Language Theory 1991年春季大会（但し、実際の報告集出版は、1992年1月）, Logic and Formal Methods Series 2, Conordia 大学出版局 20-28 1991.12

Research paper (international conference proceedings), Joint Work, Accepted

System description of LAMBDALG

Yexuan Gui and Mitsuhiro Okada

Proc. Of Logic Programming and Automated Reasoning, Springer Lecture Notes in Artificial Intelligence 698（ドイツ Springer社） 354 - 356 1991.08

Research paper (scientific journal), Joint Work, Accepted

A Computation Model for Executable Higher-Order Algebraic Specification Languages

J.-P. Jouannaud, M. Okada

Logic in　Computer Science vol. 6, IEEE Press, USA 350 - 361 1991.06

Research paper (scientific journal), Joint Work, Accepted

The Satisfaction Problem for Systems of Ordinal Notations with Subterm Property Is Decidable

J.-P. Jouannaud, M. Okada

ICALP91, LNCS510, ドイツSpringer社 455-468 1991.06

Research paper (scientific journal), Joint Work, Accepted

Girard's Phase-Semantics and Higher Order Cut-Elimination Proof

Extended Abstracts of Montreal International Workshop on Programmin Language Theory 122-139 1991.06

Research paper (international conference proceedings), Single Work, Accepted

Interrogative Sentences in Japanese, in Language

M. Okada, K. Watanabe

Information and Computation (Formal Grammer Theory Series 3), ed. Lee, Thaehakusa 社, Seoul 64-76 1991.03

Research paper (scientific journal), Joint Work, Accepted

Satisfiability of Systems of Ordinal Notations with The Subterm Property Is Decidable

Jean-Pierre Jouannaud and Mitsuhiro Okada

Lecture Notes in Computer Science 455 - 468 1991

Research paper (scientific journal)

普遍記号学の夢と現実

岡田光弘

三田哲学会編　哲学　第91巻 143-161 1990.12

Research paper (scientific journal), Single Work

A Rational for Conditional Equational Programming

Nachum Dershowitz and Mitsuhiro Okada

Theoretical Computer Science誌 91 111 - 138 1990.09

Research paper (scientific journal), Single Work, Accepted

Weak Logical Constants and Second Order Definability of the Full-Strength Logical Constants

Mitsuhiro Okada

Annals of the Japan Association for Philosophy of Science 7 163-172 1989.10

Research paper (scientific journal), Single Work, Accepted

Ordering Strutures and the Knuth-Bendix Comletion Algorithm

M. Okada and A.Steel

Proc. 29th Allerton Conference on Communication, Control and Compuring Allerton, IL, Univ. of Illinois 出版局 1989.10

Research paper (international conference proceedings), Joint Work, Accepted

Strong Normalizability for the Combined System of The Typed Lambda Calculus and an Arbitrary Convergent Term Rewrite System

Mitsuhiro Okada

Proceedings of International Conference on Algebraic and and Symbolic Computation,ACM(Association Computer Machinery) Press 357 - 363 1989.08

Research paper (international conference proceedings), Joint Work, Accepted

Temporal Object-Oriented Databases

M. Okada, Y. Quan

Proc. Advaced Daatabase System Symposium. Kyoto, Japan 1989.08

Research paper (international conference proceedings), Joint Work, Accepted

Practical Applications of Conditional term Rewriting Theory

P. Grogono, M. Okada

Proceedings of XV Latin American Conference on Informatics　/ IX Conference of Chilean Computer Society 525-540 1989.08

Research paper (international conference proceedings), Joint Work

Applications and Results of Term Rewriting Theory

P. Grogono and Mitsuhiro Okada

Proceedings of International Conference on Symbolic and Logical Computing, North Dakota 1989.06

Research paper (international conference proceedings), Joint Work, Accepted

Conditional Equational Programing and Theory of Conditional Term Rewriting

N. Dershowitz and M. Okada

Proc. Of Fifth Generarion Computer Systems, Tokyo, ICOT 337-346 1988.12

Research paper (international conference proceedings), Joint Work, Accepted

On a Theory of Weak Implications

Mitsuhiro Okada

Journal of Symbolic logic 53 200-211 1988.10

Research paper (scientific journal), Single Work, Accepted

Prolog with Modality

Mitsuhiro Okada

Proc. European Workshop on Logical Methods in AI, Roscoff, France(パリ大学第６校出版） 1988.08

Research paper (international conference proceedings), Single Work, Accepted

Logical Analysis for Theory of Conditional Rewriting

N. Dershowitz, R.Sivakmar

Springer Lecture Notes in Computer Science 308（ドイツ　Springer社） 179-196 1988.08

Research paper (scientific journal), Joint Work, Accepted

Canonical Conditional Rewrite Systems

N. Dershowitz, R.Sivakmar

9th Coｎference on Automated Deduction, Lecture Notes in Computer Science 310（ドイツ　Springer社） 538-549 1988.07

Research paper (scientific journal), Joint Work, Accepted

Confluence of Conditional Rewrite systems

N. Dershowitz, M. Okada and G. Sivakumar

Springer　LNCS 308, ドイツ　Springer社 1988.06

Research paper (scientific journal), Joint Work, Accepted

Proof-Theoretic Techniques for Term Rewriting Theory

N. Dershowitz and M. Okada

Logic in Computer Science vol.3 IEEE Press 104-111 1988.06

Research paper (scientific journal), Joint Work, Accepted

Notes on Proof of the Extended Kirby-Paris Theorem on Labeled Finite Trees

Mitsuhiro Okada

European Journal of Conbinatorics 9 ( 3 ) 249 - 253 1988

Research paper (scientific journal), Single Work, Accepted

A Weak Intuitionistic Propositional Logic with Purely Constructive Implication

Mitsuhiro Okada

Studia Logica 46 ( 4 ) 371 - 382 1987.12

Research paper (scientific journal), Single Work, Accepted

A simple relationship between Buchholz's new system of ordinal notations and Takeuti's system of ordinal diagrams

Mitsuhiro Okada

Journal of Symbolic Logic 52 577-581 1987.09

Research paper (scientific journal), Single Work, Accepted

論理記号導入規則による論理的意味論について

岡田光弘

科学基礎論研究68、　日本科学基礎論学会 65-71 1987.06

Research paper (scientific journal), Single Work, Accepted

初期フッサールの「数理－哲学的研究の最終テーマ」とゲッチンゲン学派の論理哲学

岡田光弘

哲学37 　日本哲学会 210-221 1987.05

Research paper (scientific journal), Single Work, Accepted

Finite Combinatorics

Mitsuhiro Okada

Combinatorics (American Mathematical Society) 8 1987

Research paper (other academic)

On The Theory of Quasi-Ordinal Diagram

Mitsuhiro Okada and Gaisi Takeuti

Contemporary Mathematics (American Mathematical Society) 65 295 - 308 1987

Research paper (international conference proceedings)

形式的意味論と整合性証明

岡田光弘

哲学(1986)　三田哲学会 1986.12

Research paper (scientific journal), Single Work

　 Previous page - Next page 　