論文 - 岡田　光弘

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月

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

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月

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