Papers - Okada, Mitsuhiro

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

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

　View Summary

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

　View Summary

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

　View Summary

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

　View Summary

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

　View Summary

© 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

　View Summary

© 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

　View Summary

© 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