"Logical Inference and Proofs" Franco-Japanese Workshop
- 2015年1月12日(月)13:00〜18:00 / 13日(火) 10:00〜16:00 (*開始時間変更の可能性あり．)
- January 12th (13:00-18:00) / 13th (10:00-17:00), 2015
- 慶應義塾大学三田キャンパス 東館6階G-Sec Lab (最寄駅:JR 田町、地下鉄三田又は赤羽橋) (キャンパスマップ) なお月曜日は祝日のため東門は閉門しています．東館の入口扉は開錠しているはずですが，万が一閉まっている場合は，お手数ですが正門にお回りください．
- G-Sec Lab, 6th Floor of East Research Building, Mita campus of Keio University. (Campus Map) *Notice: The first day is the national holiday and the east gate should be closed for the day. So if the entrance of the first floor of East Building is closed, please come through the main gate of the campus to reach the East Building.
参加方法：参加費無料．会場準備のため氏名、所属を明記して「Logical Inference and Proofs 集会参加希望」と件名を記したメールを事務局 logic[AT]abelard.flet.keio.ac.jp 宛に 1/9 までにお送りください。(※12日セッション終了後のレセプションも参加自由です。)
- Pierre Wagner (University of Paris I and Institute of History and Philosophy of Science) 論理哲学
- Jean-Baptiste Joinet (University of Lyon III and Centre Cavaillès, ENS-Paris) 線形論理
- Gilles Dowek (INRIA) タイプ理論・定理自動証明
- Jérôme Prado (University of Lyon I -- CNRS, Language-Brain-Cognition Lab) 推論の認知神経科学
- Alberto Naibo (University of Paris I and Institute of History and Philosophy of Science) 証明と計算の論理
- Philippe Codognet (CNRS-Tokyo Joint Lab Director, University of Paris VI)
- Shigeru Watanabe (Keio University)
- Kazushige Terui (Mathematical Science Institute, Kyoto University) 情報論理
- Koji Mineshima (Center for Simulation Science, Ochanomizu University) 自然言語意味論
|13:00 Opening Remark|
|12:30-14:00 Lunch Break|
- Jean-Baptiste Joinet
- The computational basis of semantics
In this talk, I will focus on the abstract minimal conditions under which computational processes are in order to generate meaning: I will then stress in which way such an approach of the semantical question, combined with the Formulas-as-Types approach (Proofs-as-Programs paradigm), permits to overcome the two major obstacles that the standard proof-theoretical approach of meaning theory encounters.
- Kazushige Terui
- Algebraic aspects of proof theory in nonclassical logics
Hypersequent calculus, introduced by Arnon Avron, is an extension of the ordinary sequent calculus that deals with disjunctions of sequents. Historically it has been a tool for studying intermediate logics and many-valued logics (so-called fuzzy logics), but it is interesting in its own right as proof system with a well-behaved cut-elimination procedure. In this talk, I will discuss some aspects of hypersequents in the context of substructural logics (axiomatic extensions of full Lambek calculus), that could be meaningful to those who are not interested in fuzziness at all. The topics include: * Brouwer's fixed point theorem and cut-elimination: a potential link. * Algebraic cut-elimination a la Maehara and Okada: success and limitation. * Cut-elimination and Herbrand's theorem: an algebraic perspective.
- Gilles Dowek
- Creation and automation in proofs
In many intellectual activities, we can distinguish a creative part and an less creative one, where a known method is automatically applied. We shall discuss how this distinction can be reflected in proofs and how this simplifies proof-search algorithms.
- Pierre Wagner
- Logic and normativity
Logic is often regarded as a normative science, as opposed to a descriptive science, and the philosophical discussions about the normativity of logic have often focused on the traditional idea of logic as providing the laws of thought. However, logic is now regarded as concerned in an essential way with proofs and computations. The question may then be raised of the normative content of logic in this new context. In this talk, I shall examine the sense in which logic may be said to be normative and raise the issue of the relevance of contemporary philosophical discussions about the normativity of logic from this viewpoint.
- Alberto Naibo
- Typed vs. untyped proof theory
Two different ways of understanding the notion of proof are investigated. The first considers proofs as linguistic typed entities and tries to build an inferential theory of meaning on them. The second studies proofs with respect to their computational features and aims at the development of a theory of ``pure'', or untyped, constructions. It is argued that some very recent developments in proof theory, as J.-Y. Girard's geometry of interaction, can be seen as part of the latter conception, generalizing a programme initiated by G. Kreisel and N.D. Goodman in the seventies.
- Koji Mineshima
- Types in natural language semantics
Type theories have provided powerful tools and concepts for the study of natural language semantics. The recent advances show that the notion of types not only provides general principles underlying the compositional derivation of sentence meanings, but can also play a role in the analysis of natural language inferences under the paradigm of propositions-as-types. In particular, dependent types provide rich type structures that can be applied to a variety of dynamic phenomena in natural language. In this talk, I will present some recent developments, focusing on topics such as anaphora and presupposition, and discuss prospects for applying these results to the study of textual inferences in the context of computational linguistics.
- Shigeru Watanabe
- Divergence of logics in animal
Logic is formalization of human way of thinking in its origin. Humans and non-human animals display rational behavior but they sometime show irrational behavior also. These rational/irrational behaviors are products of phylogenetic contingency (evolution) and recent development in comparative cognition study provides evidences suggesting divergence of logics in animal kingdom. I will present similarity and dissimilarity of human logic and animal logic and criticize an idea that “logic” is human unique ability.
- Jérôme Prado
- The brain network for deductive reasoning
Deductive reasoning is the process of drawing conclusions that are guaranteed to follow from given premises. Perhaps because deductions are an essential element of human thinking, the study of deductive reasoning has been central to the cognitive literature for over 50 years. The emergence of neuroimaging techniques two decades ago held the promise of using information about the neural basis of deductive reasoning to inform cognitive theories of deductive reasoning. In this talk, I will review findings from neuroimaging studies in healthy adults and discuss how they relate to theories of deductive reasoning. I will also present a recent study examining the neural development of deductive reasoning in school-age children. Finally, I will discuss the implications of this research for improving our understanding of learning disabilities in children.
- Kiyomi Yatabe
- Maturational cerebral hemodynamic changes in the prefronto-parietal regions used in relational reasoning among participants from late childhood to young adulthood
Relational reasoning, i.e. categorization of newly experienced objects according to past experience and recognition of the relations between them, is fundamental to human cognition and intelligence, and requires keeping objects in memory and finding higher order relations between them. In this talk, we will report on experiments concerning maturational changes in relational reasoning among young participants aged 8 to 21 years old, which used behavioral and brain-function measurements involving near-infrared spectroscopy (NIRS).
- Yuri Sato
- Counter-example construction in human diagrammatic reasoning
In this talk, I will explore the question whether people really reason by counter-example construction. To clarify the cognitive potentials of logical inference, my approach focuses on "diagrammatic reasoning". I introduce a method of asking reasoners to directly manipulate diagrammatic objects as a component of inferential processes, and observe how reasoners move diagrams to check the (in)validity of inference.
公開日時: December 25, 2014 12:38