論文 - 岡田　光弘

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月

最終著者, 査読有り

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

Mathieu Marion and Mitsuhiro Okada

Routledge Studies in Twentieth-Century Philosophy) H 230 （Routledge）  230   1 - 16 2023年02月

論文集(書籍)内論文, 共著, 責任著者

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.

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)）  12328 LNCS   136 - 155 2020年

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.

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)）  12169 LNAI   365 - 381 2020年

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.

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)）  12300 LNCS   39 - 47 2020年

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月

研究論文（学術雑誌）, 査読有り,  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

岡田 光弘 高橋　優太

Electronic Proceedings of Theoretical Computer Science (EPTCS), 288, Post-Workshop Proceedings of the 10th Workshop on Computation with Terms and Graphs (TermGraph 2018), （EPTCS）     38 - 49 2019年03月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

Following a Rule: Waismann's Version

<Uマリオン, >マシュー岡田 光弘(/)-#HR

Publications of the Austrian Ludwig Wittgenstein Society – New Series （Austrian Ludwig Wittgenstein Society）  2019年

研究論文（国際会議プロシーディングス）, 共著

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 （Prontiers）  8(AUG), [1388]. 2017年08月

研究論文（学術雑誌）, 共著, 査読有り

• Access to Document (DOI)

What is logic?

Mitsuhiro Okada

Proceedings of "Beyond Logic" cericy Meeting May 21-May 26, 2017 （Cersy）  2017年07月

研究論文（国際会議プロシーディングス）, 単著

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月

研究論文（国際会議プロシーディングス）, 査読有り

• 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月

研究論文（学術雑誌）, 共著, 査読有り

• Access to Document (DOI)

初期フッサールの普遍算術と確定多様体について : 1901年冬草稿

岡田 光弘

現象学年報 （日本現象学会）  31   1 - 15 2015年11月

研究論文（学術雑誌）, 単著

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年

研究論文（学術雑誌）, 共著, 査読有り

• 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月

研究論文（学術雑誌）, 共著, 査読有り

Wittgenstein on Equinumerosity and Surveyability

M. Marion and M. Okada

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

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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月

研究論文（国際会議プロシーディングス）, 共著

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月

研究論文（学術雑誌）, 共著

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月

研究論文（学術雑誌）, 共著

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年

研究論文（国際会議プロシーディングス）, 単著

Shape Perception in Chemistry

Janna Hastings, Colin Batchelor and Mitsuhiro Okada

CEUR Proceedings 2013年

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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年

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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年

研究論文（学術雑誌）, 共著, 査読有り

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年

研究論文（学術雑誌）, 共著

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年

研究論文（学術雑誌）, 共著, 査読有り

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年

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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

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

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

研究論文（その他学術会議資料等）, 共著

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 Watanabe

Behavioural Brain Research ???volume??? 210 号 2 （Behavioural Brain Research）  6   178 - 183 2010年07月

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

岡田 光弘

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

研究論文（学術雑誌）, 単著

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

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

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

研究論文（その他学術会議資料等）, 共著

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年

研究論文（学術雑誌）, 共著, 査読有り

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

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

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

研究論文（学術雑誌）, 共著, 査読有り

Secrecy-Oriented First-Order Logical Analysis of Cryptographic Protocols

Gergei Bana, Koji Hasebe, and Mitsuhiro Okada

IACR Cryptology ePrint Archive 2010年

研究論文（その他学術会議資料等）, 共著

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年

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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年

研究論文（学術雑誌）, 共著, 査読有り

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年

研究論文（学術雑誌）, 共著, 査読有り

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年

研究論文（学術雑誌）, 単著, 査読有り

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年

研究論文（学術雑誌）, 共著, 査読有り

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

岡田光弘

「現代思想」Vol.35, No.3    149 - 163 2007年02月

研究論文（学術雑誌）, 単著

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年

研究論文（学術雑誌）, 共著, 査読有り

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年

研究論文（学術雑誌）, 共著, 査読有り

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年

研究論文（学術雑誌）, 共著, 査読有り

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

長谷部浩二、岡田光弘.

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

研究論文（学術雑誌）, 共著, 査読有り

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年

研究論文（学術雑誌）, 共著, 査読有り

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

岡田 光弘，長谷部 浩二

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

研究論文（国際会議プロシーディングス）, 共著, 査読有り

Honesty Inferences for Proving Correctness of Security Protocols

岡田 光弘，長谷部　浩二

Workshop on New Approaches to Software Construction (WNASC 2004)    45-57 2004年09月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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

岡田 光弘，長谷部 浩二

Workshop on Foundations of Computer Security (FCS'04)    97-113 2004年07月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

Inferences on Honesty in Compositional Logic for Security Analysis

岡田 光弘，長谷部 浩二

the International Symposium on Software Security 2003 (ISSS2003)    65-86 2004年06月

研究論文（国際会議プロシーディングス）, 共著, 査読有り,  ISSN  0302-9743

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

岡田 光弘

科学哲学 36 （ 2 ） 79-102 2004年

研究論文（学術雑誌）, 単著, 査読有り

Linear Logic and Intuitionistic Logic

Mitsuhiro Okada

La revue International de philosphie  （ 230 ） 449-481 2004年

研究論文（学術雑誌）, 単著, 査読有り

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月

研究論文（その他学術会議資料等）, 共著

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

Mitsuhiro Okada

Theoretical Computer Science 294 （ 3 ） 551 - 573 2003年02月

研究論文（学術雑誌）, 共著, 査読有り

Linear Logic

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

Theoretical Computer Science 294 （ 3 ）  2003年02月

研究論文（学術雑誌）, 単著, 査読有り

Preface

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

Theoretical Computer Science 294 （ 3 ）  2003年

研究論文（学術雑誌）, 共著

Phase Semantics for Light Linear Logic

M. Konovitch, A. Scedrov, Mitsuhiro Okada

Thoretical Computer Science 294   525-549 2003年

研究論文（学術雑誌）, 共著, 査読有り

　概要を見る

実現可能計算量を特徴付ける線形論理の部分体系に対する意味論的分析を与えた。

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年

研究論文（学術雑誌）, 共著, 査読有り

　概要を見る

非可換線形論理のプルーフネットのグラフ論的特長付けを与えた。

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年

研究論文（学術雑誌）, 単著, 査読有り

　概要を見る

クリプキ可能世界解釈の述語論理への埋め込み定理の証明

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

岡田 光弘

人工知能学会誌 17 （ 5 ） 604-613 2002年09月

研究論文（学術雑誌）, 単著

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

岡田 光弘

人工知能学会誌 17 （ 4 ） 434-442 2002年07月

研究論文（学術雑誌）, 単著

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月

研究論文（学術雑誌）, 単著, 査読有り

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

岡田 光弘

人工知能学会誌 Vol.17 （ No.3 ） 335-344 2002年05月

研究論文（学術雑誌）, 単著, 査読有り

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

溝口 理一郎, 岡田 光弘.

人工知能学会誌 17 （ 2 ） 224 - 231 2002年03月

研究論文（学術雑誌）, 共著

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

岡田 光弘

人工知能学会誌 Vol.17 （ No.2 ） 224-231 2002年03月

研究論文（学術雑誌）, 単著, 査読有り

Preface

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

Theoretical Computer Science 272 （ 1--2 ） 1 - 2 2002年02月

研究論文（学術雑誌）, 共著, 査読有り

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

岡田 光弘, 長谷部浩二

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

研究論文（その他学術会議資料等）, 共著

Inductive Date Type Systems

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

Thoretical Computer Science 272   41-68 2002年

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（学術雑誌）, 単著, 査読有り

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月

研究論文（学術雑誌）, 単著, 査読有り

The Finite Model Property for Various Fragments of Intuitionistic Linear Logic

M. Okada, K. Terui

Journal of Symbolic Logic 64   790 - 802 1999年03月

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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年

研究論文（学術雑誌）, 共著, 査読有り

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年

研究論文（その他学術会議資料等）, 共著

Abstract Data Type Systems

J.-P. Jouannaud, M. Okada

Theoretical Computer science 173 (欧州理論情報学会誌）,    349-391 1997年12月

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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

M,Hamano, M. Okada

Mathematical Logic Quarterly 43    103-120 1997年03月

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（その他学術会議資料等）, 共著

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月

研究論文（その他学術会議資料等）, 共著

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

岡田 光弘

哲學　三田哲学会編  （ 101 ） 1 - 43 1997年

研究論文（学術雑誌）, 単著

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

哲学　三田哲学会編  （ 第100号 ） 63-86 1996年10月

研究論文（学術雑誌）, 単著

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月

研究論文（学術雑誌）, 共著, 査読有り

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

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

研究論文（学術雑誌）, 単著

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月

研究論文（学術雑誌）, 単著, 査読有り

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月

研究論文（国際会議プロシーディングス）, 共著

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年

研究論文（その他学術会議資料等）

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

岡田 光弘

三色旗　慶應義塾大学通信教育部 1994年06月

単著

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

岡田 光弘

三田評論 1994年04月

単著

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月

研究論文（その他学術会議資料等）, 共著

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

Mitsuhiro Okada

三田哲学会編　哲学 第95巻   1-14 1993年12月

研究論文（学術雑誌）, 単著

LAMBDALG-Higher Order Algebraic Specification Language

Y.Gui, M. Okada

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

研究論文（学術雑誌）, 共著, 査読有り

教育と社会

岡田光弘

三色旗　慶應義塾大学通信教育部 1993年05月

単著

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月

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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月

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（学術雑誌）, 共著, 査読有り

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

Extended Abstracts of Montreal International Workshop on Programmin Language Theory    122-139 1991年06月

研究論文（国際会議プロシーディングス）, 単著, 査読有り

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月

研究論文（学術雑誌）, 共著, 査読有り

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年

研究論文（学術雑誌）

普遍記号学の夢と現実

岡田 光弘

三田哲学会編　哲学　第91巻    143-161 1990年12月

研究論文（学術雑誌）, 単著

A Rational for Conditional Equational Programming

Nachum Dershowitz and Mitsuhiro Okada

Theoretical Computer Science誌 91    111 - 138 1990年09月

研究論文（学術雑誌）, 単著, 査読有り

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月

研究論文（学術雑誌）, 単著, 査読有り

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月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

Temporal Object-Oriented Databases

M. Okada, Y. Quan

Proc. Advaced Daatabase System Symposium. Kyoto, Japan 1989年08月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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月

研究論文（国際会議プロシーディングス）, 共著

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月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

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月

研究論文（国際会議プロシーディングス）, 共著, 査読有り

On a Theory of Weak Implications

Mitsuhiro Okada

Journal of Symbolic logic 53    200-211 1988年10月

研究論文（学術雑誌）, 単著, 査読有り

Prolog with Modality

Mitsuhiro Okada

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

研究論文（国際会議プロシーディングス）, 単著, 査読有り

Logical Analysis for Theory of Conditional Rewriting

N. Dershowitz, R.Sivakmar

Springer Lecture Notes in Computer Science 308（ドイツ　Springer社）    179-196 1988年08月

研究論文（学術雑誌）, 共著, 査読有り

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月

研究論文（学術雑誌）, 共著, 査読有り

Confluence of Conditional Rewrite systems

N. Dershowitz, M. Okada and G. Sivakumar

Springer　LNCS 308, ドイツ　Springer社 1988年06月

研究論文（学術雑誌）, 共著, 査読有り

Proof-Theoretic Techniques for Term Rewriting Theory

N. Dershowitz and M. Okada

Logic in Computer Science vol.3 IEEE Press    104-111 1988年06月

研究論文（学術雑誌）, 共著, 査読有り

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

Mitsuhiro Okada

European Journal of Conbinatorics 9 （ 3 ） 249 - 253 1988年

研究論文（学術雑誌）, 単著, 査読有り

A Weak Intuitionistic Propositional Logic with Purely Constructive Implication

Mitsuhiro Okada

Studia Logica 46 （ 4 ） 371 - 382 1987年12月

研究論文（学術雑誌）, 単著, 査読有り

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月

研究論文（学術雑誌）, 単著, 査読有り

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

岡田 光弘

科学基礎論研究68、　日本科学基礎論学会    65-71 1987年06月

研究論文（学術雑誌）, 単著, 査読有り

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

岡田 光弘

哲学37 　日本哲学会    210-221 1987年05月

研究論文（学術雑誌）, 単著, 査読有り

Finite Combinatorics

Mitsuhiro Okada

Combinatorics （American Mathematical Society）  8 1987年

研究論文（その他学術会議資料等）

On The Theory of Quasi-Ordinal Diagram

Mitsuhiro Okada and Gaisi Takeuti

Contemporary Mathematics （American Mathematical Society）  65   295 - 308 1987年

研究論文（国際会議プロシーディングス）

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

岡田 光弘

哲学(1986)　三田哲学会 1986年12月

研究論文（学術雑誌）, 単著