Logic-ml

9 participants
1781 discussions

Fwd: CAPEロジック・ワークショップ：講演追加のお知らせ
by 矢田部俊介 12 Sep '12

12 Sep '12

# 複数受け取られた場合はご容赦ください。 2012年9月18日（火）に京都大学文学研究科附属応用哲学・倫理学教育研究センター（CAPE）の主催にて開催されるCAPEロジック・ワークショップに、以下の講演が追加されます。 17:15-18:15 Greg Restall "Logical Constants and Focusing Disagreements" ご案内として以下をご転送いたします。皆様のご参加をお待ち申し上げます。矢田部俊介 ---------- Forwarded message ---------- From: Toshihiko TAKENAKA <t-take(a)rj8.so-net.ne.jp> Date: 2012/9/12 Subject: CAPEロジック・ワークショップ：講演追加のお知らせ To: CAPE(a)bun.kyoto-u.ac.jp 皆様 2012年9月18日（火）に京都大学文学研究科附属応用哲学・倫理学教育研究センター（CAPE）の主催にて開催されるCAPEロジック・ワークショップですが、以下の講演が追加されました。 17:15-18:15 Greg Restall "Logical Constants and Focusing Disagreements" 皆様のご参加をお待ち申し上げます。京都大学大学院文学研究科附属応用哲学・倫理学教育研究センター http://www.bun.kyoto-u.ac.jp/cape/cape-top_page/ 事務補佐　　竹中利彦〒606-0085 京都市左京区吉田本町　京都大学文学部内 CAPE(a)bun.kyoto-u.ac.jp --- 記 --- CAPEロジック・ワークショップ日時：2012年9月18日（火） 10時30分〜18時15分場所：京都大学文学部校舎二階第六講義室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm （8番の建物です）講演者・題目： 10:30-12:00 大西琢郎　 "Usefulness of deduction and Proof-Theoretic Semantics" 13:30-15:00 Shawn Standefer: "Truth and conditionals" 15:30-17:00 丸山善宏 "Categorical Harmony and Degrees of Paradoxity" 17:15-18:15 Greg Restall "Logical Constants and Focusing Disagreements" **************************************************************************** ********** CAPE Logic workshop Date : September 18 (Tuesday) Place:　 The 6th lecture room, 2nd floor, Faculty of letters, Kyoto University (building no.6 of the following map) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm *Schedule: 10:30-12:00 Takuro Onishi: "Usefulness of deduction and Proof-Theoretic Semantics" 13:30-15:00 Shawn Standefer: "Truth and conditionals" 15:30-17:00 Yoshihiro Maruyama: "Categorical Harmony and Degrees of Paradoxity" 17:15-18:15 Greg Restall "Logical Constants and Focusing Disagreements" *Abstracts (1)Speaker: Takuro Onishi Title: Usefulness of deduction and Proof-Theoretic Semantics Abstract: Michael Dummett’s anti-realist theory of meaning is considered to provide a philosophical basis of proof-theoretic semantics, which is an inferentialis approach to logical validity. Unfortunately, in the debate of proof-theoretic semantics, due attention has not been paid to his fundamental consideration on the nature of deductive inference, in which he emphasizes its usefulness or fruitfulness as well as its validity. That is, deduction is a special kind of activity of extending our knowledge. Dummett represents it as involving a certain tension between validity and usefulness, and tries to reconcile it against the background of his own meaning theory. In this talk I present Dummett’s view on deduction, and compare it with G.Restall’s bilateralist explication of logical consequence which would justify classical logic. (2)Speaker: Shawn Standefer Title: Truth and conditionals Abstract: Some recent approaches to truth have adopted the strategy of enriching the underlying logic with a new conditional. I will provide some background on these approaches and distinguish different roles that such conditionals play in the theory. I will show how this distinction plays out in an extension of the revision theory of truth and use the distinction to offer a philosophical defense of that theory. (3)Speaker: Yoshihiro Maruyama Title: Categorical Harmony and Degrees of Paradoxity Abstract: Prior's weird connective "tonk" compelled logicians to articulate the concept of a logical constant, eventually giving rise to developments of proof-theoretic semantics in the spirit of inferentialism, and to the notion of proof-theoretic harmony in particular, which works as a criterion to judge if a connective is a proper logical constant or not. Different concepts of harmony have been proposed and discussed by Belnap, Dummett, and many others. Building upon Lawvere's understanding of logic via category theory, I formulate a categorical concept of harmony relativised to primitive vocabulary, and compare it with other notions of harmony. The categorical conception of harmony leads us to a novel analysis of the nature of tonk: namely, the problem of tonk is the problem of equivocation in terms of adjoint functors. It finally turns out that there are different degrees of paradoxity of logical constants from a categorical perspective. (4)Speaker: Greg Restall Title: Logical Constants and Focusing Disagreements Abstract: For expressivists about logic (such as Robert Brandom and Jaroslav Peregrin), logical vocabulary gives us means to do more than we could without it. With concepts such as negation, conjunction, conditionality, and the quantifiers, we can express contents which would otherwise be out of reach to us. However, in another sense, logical vocabulary seems to be neutral with regard to content. It does not seem to add any new subject matter to our thoughts or conversations. I will attempt to explain why a certain class of logical expressions (including the standard propositional connectives, first order quantifiers, and perhaps some modal operators) give us means to extend our expressive resources without adding new subject matter, by attending to the role special that logical vocabulary can play in articulating disagreements.

1 0

Final CFP: JURISIN2012
by Makoto Nakamura 11 Sep '12

11 Sep '12

（重複して受け取られた場合はご容赦ください）名古屋大学の中村と申します。法情報学に関する国際ワークショップ JURISIN2012 の Final CFP をお送りします。今年の１１月３０日から１２月１日にかけて宮崎で開催されます。投稿締め切りが９月２４日まで延長されましたので、多数のご投稿をお待ちしております。 [Apologies for multiple copies] --------------------------------------------------- Final Call for Papers (Deadline extended to Sep 24, 2012): Sixth International Workshop on Juris-informatics (JURISIN 2012) Nov.30 - Dec. 1, 2012 http://www.kl.i.is.nagoya-u.ac.jp/jurisin2012/ Amusement Zone Miyazaki (The JA-AZM Hall) Kirishima 1-1-1, Miyazaki, Japan with a support of The Japanese Society for Artificial Intelligence in association with Fourth JSAI International Symposia on AI (JSAI-isAI 2012) **** Submission Deadline: September 24, 2012 (extended) **** **** Aims and scope **** Juris-informatics is a new research area which studies legal issues from the perspective of informatics. The purpose of this workshop is to discuss both the fundamental and practical issues for juris-informatics among people from the various backgrounds such as law, social science, information and intelligent technology, logic and philosophy, including the conventional "AI and law" area. We solicit unpublished papers on theories, technologies and applications on juris-informatics. **** Topics **** Relevant topics include, but are not limited to, the following: * Legal reasoning * Argumentation/Argumentation agent * Legal term ontology * Formal legal knowledge-base/Intelligent management of legal knowledge-base * Translation of legal documents * Computer-aided law education * Use of Informatics and AI in law * Legal issues on ubiquitous computing/multi-agent system/the Internet * Social implications of use of informatics and AI in law **** Submissions **** We welcome and encourage the submission of high quality, original papers, which are not simultaneously submitted for publication elsewhere except as a submission to JURIX 2012 (The 25th International Conference on Legal Knowledge and Information Systems). The double submission policy with JURIX 2012 is as follows: 1. Papers being submitted both to JURISIN2012 and JURIX2012 must note this on the title page. 2. A paper to be presented at JURISIN2012 must be withdrawn from JURIX2012 and vice versa according to the choice by the authors. 3. If the authors do not follow this double submission policy, the paper by the authors will not be included in the proceedings of JURISIN 2012. Papers should be written in English, formatted according to the Springer Verlag LNCS style in a pdf form, which can be obtained from http://www.springeronline.com, and not exceed 14 pages including figures, references, etc. If you use a word file, please follow the instruction of the format designated at the workshop page, and then convert it into a pdf form and submit it at the paper submission page. If a paper is accepted, at least one author of the paper must register the workshop and present it. **** Invited Speakers **** 1. Kazuhisa Todayama (Professor, Graduate School of Information Science, Nagoya University, Japan) 2. Philip T H Chung (Executive Director, Australasian Legal Information Institute, Australia) and Graham Greenleaf (Professor, Faculty of Law, University of New South Wales, Australia) **** Proceedings **** A printed volume of the proceedings with ISBN will be available at the workshop. **** Post Proceedings**** The chair of JSAI-IsAI 2012 is now negotiating with Springer Verlag to publish selected papers of the workshop in the JSAI-isAI 2012 post-proceedings as a volume of LNAI. If it is the case, the authors of papers presented at the workshop will be asked to extend their contributions, possibly incorporating the results of the workshop discussion, to be included in the workshop post-proceedings, after another round of refereeing. Note that the selected papers of the previous workshops were publisehd as volumes of LNAI4914(JURISIN 2007), LNAI5447(JURISIN 2008), LNAI6284(JURISIN 2009), LNAI6797(JURISIN2010) and LNAI7258(JURISIN2011), respectively. **** Financial Support for Students **** We have received from JSAI partical economical support for travelling costs for promising foreign students whose papers have been accepted to be presented at JURISIN2012. The amount of the whole support is 250,000 yen and we divide it to students who need a support. The actual support will vary based on the number of applicants and where students come from. Please contact the chairperson (mnakamur ((at)) law.nagoya-u.ac.jp) for details. **** Important Dates **** Submission Deadline: September 24, 2012 (extended) Notification: October 22, 2012 (extended) Camera Ready Copy due: November 5, 2012 (extended) JURISIN 2012: November 30 - December 1, 2012 **** Workshop Chair **** Makoto Nakamura, Nagoya University, Japan Katsuhiko Toyama, Nagoya University, Japan **** Organizing Committee Members **** Makoto Nakamura, Nagoya University, Japan Katsumi Nitta, Tokyo Institute of Technology, Japan Seiichiro Sakurai, Meiji Gakuin University, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Satoshi Tojo, Japan Advanced Institute of Science and Technology(JAIST), Japan Katsuhiko Toyama, Nagoya University, Japan **** Programme Committee Members **** Thomas Agotnes, University of Bergen, Norway Marina De Vos, University of Bath, UK Phan Minh Dung, AIT, Thailand Tom Gordon, Franfoher FOKUS, Germany Guido Governatori, The University of Queensland, Australia Tokuyasu Kakuta, Nagoya University, Japan Takehiko Kasahara, Toin University of Yokohama, Japan Masahiro Kozuka, Kanazawa University, Japan Makoto Nakamura, Nagoya University, Japan Katsumi Nitta, Tokyo Institute of Technology, Japan Paulo Novais, University of Minho, Portugal Jeremy Pitt, Imperial College, UK Henry Prakken, University of Utrecht & Groningen, The Netherlands Seiichiro Sakurai, Meiji Gakuin University, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Akira Shimazu, Japan Advanced Institute of Science and Technology, Japan Fumihiko Takahashi, Meiji Gakuin University, Japan Satoshi Tojo, Japan Advanced Institute of Science and Technology, Japan Katsuhiko Toyama, Nagoya University, Japan Radboud Winkels, The University of Amsterdam, the Netherlands Shin-ichi, Yoro, Osaka University, Japan John Zeleznikow, Victoria University, Australia **** Home page of JURISIN 2012 **** http://www.kl.i.is.nagoya-u.ac.jp/jurisin2012/ **** preivous JURISIN workshops **** JURISIN2007 http://research.nii.ac.jp/~ksatoh/jurisin.html JURISIN2008 http://www.ntt.dis.titech.ac.jp/jurisin2008/ JURISIN2009 http://research.nii.ac.jp/~ksatoh/jurisin2009.html JURISIN2010 http://research.nii.ac.jp/~ksatoh/jurisin2010.html JURISIN2011 http://research.nii.ac.jp/~ksatoh/jurisin2011.html For any inquiry, please send it to "jurisin2012 ((at)) kl.i.is.nagoya-u.ac.jp".

1 0

SLACS2012参加案内およびプログラム（9/9 ver. 再送）
by Hiroyuki Miyoshi 10 Sep '12

10 Sep '12

（メールが一部上手く届かないようなので再送致します。重複された方は申し訳ありません。） SLACS2012講演者の方々および参加者を考慮されている皆様， 9/15-16に開催されるSLACS2012の参加案内およびプログラムの 9/9 ver.をお送りします。前回との変更点は以下の通りです。 * 司会のことを考慮して9/16の蓮尾一郎さん，丸山善宏さん， Michele Basaldellaさんの順序を変更しました。もしご都合が悪ければご連絡をよろしくお願いいたします。 * 蓮尾一郎さん，小林聡さん，佐藤雅大の講演時間短縮をなくしました。既に研究会直前ですので前回のアナウンス通りに 15分以上短縮されても昼食や終了が前倒しになるだけで大丈夫なようにしてあります。講演予定に合わせてお決め下さい。 * 懇親会の時間を30分繰り上げました。なお，ウェブページを作成いたしましたので今後の変更はそちらに反映していきます。 http://www.cc.kyoto-su.ac.jp/~hxm/slacs2012.html ---------------------------------------------------------- SLACS2012研究会への参加案内第29回記号論理と情報科学研究集会 (SLACS 2012) は，京都産業大学むすびわざ館で開催の予定です．SLACSは，記号論理学とコンピュータ科学の研究者や学生の相互交流を目的として開催されている研究集会で毎年持ち回りで行われています（http://www.math.s.chiba-u.ac.jp/SLACS/）。完成された研究のみならず，発展途上の話題やサーベイなども大歓迎です．記号論理以外にも，圏論やアルゴリズム理論などコンピュータ科学に関わる講演が広く行われます。開催要項開催日：2011年9月15日（土）13:00 〜 9月16日（日）18:20 場所：京都産業大学むすびわざ館〒600-8533 京都市下京区中堂寺命婦町1-10 Tel.075-277-1600　Fax.075-277-1699 （京都産業大学神山キャンパスとは異なります） http://www.kyoto-su.ac.jp/outline/shisetsu/musubiwaza/ アクセス：最寄り駅はJR丹波口駅および阪急大宮駅 http://www.kyoto-su.ac.jp/outline/shisetsu/musubiwaza/access.html 研究会参加について申し込みも費用も不要です（懇親会については後述）。皆様ふるってご参加よろしくお願いいたします。懇親会は9月15日18:00-20:00に予定しています．かごの屋五条七本松店 075-326-1165 http://www.kinrei.com/shop/spec/?shop_id=42 http://r.gnavi.co.jp/k539974/ （ぐるなび）懇親会の参加・不参加については事前に三好（hxm(a)cc.kyoto-su.ac.jp) まで連絡して頂けると助かります。（9/15の15:00頃に人数を確定して私が店に連絡致します。予算3-4千円程度）。梗概については本研究会のウェブページ http://www.cc.kyoto-su.ac.jp/~hxm/slacs2012.html を御覧下さい。現在まだ，題目・梗概が未定の方は連絡をよろしくお願い致します。 ---- 世話人：京都産業大が理学部数理科学科三好博之 hxm(a)cc.kyoto-su.ac.jp ---------------------------------------------------------- SLACS2012 プログラム 9/15（土曜日） 13:00-13:30 三角形に関する平面ユークリッド幾何への数式処理の応用鴨浩靖，萩尾由貴子，溝口涼子（講演者）（奈良女子大学理学部） 13:35-14:05 オラクルの圏論的記述―終対象の一般化として― 吉村和人（JAIST） 14:10-14:40 Rewriting Apploaches to Computational Complexity and Complexity 江口直日（東北大学理学研究科） 14:40-15:00 休憩20分 15:00-15:30 論理CDの補完定理について河野友亮（東京工業大学情報理工学研究科） 15:35-16:05 様相Lukasiewicz論理の公理化について岩波克（東京工業大学情報理工学研究科） 14:40-15:00 休憩20分 16:10-16:40 Non-Commutative First-Order Sequent Calculus 龍田真（国立情報学研究所） 16:45-17:15 TLCA未解決問題20番: 遺伝的置換子の型龍田真（国立情報学研究所） 17:15-17:30 ビジネスミーティング（次回開催について） 18:00-20:00 懇親会 9/16（日曜日） 10:00-11:00 Duality, Quantum Symmetry and Categorical Logic 丸山善宏（Oxford University） 11:10-12:10 Nonstandard Static Analysis: Discrete Verification Methodologies 蓮尾一郎（東京大学情報理工学研究科） 12:10-13:30 昼食 13:30-14:15 An interactive semantics for classical arithmetic (in English) Michele Basaldella (JAIST) 14:15-15:00 On some variants of the Jayne-Rogers THeorem via the 木原貴行(JAIST) 15:05-15:35 ゲーム論的確率論入門宮部賢志（京都大学数理解析研究所） 15:35-15:55 休憩20分 15:55-16:40 戦略的論理式松尾亮太（名古屋大学大学院情報科学研究科計算機数理科学専攻） 16:45-17:30 未定小林聡（京都産業大学コンピュータ理工学部） 17:35-18:35 未定（Coqによる数学について）佐藤雅大（名古屋大学多元数理科学研究科） 18:35-18:40 次回予定アナウンスおよび挨拶 ----

1 0

SLACS2012プログラムおよび梗概(9/9 ver.)
by Hiroyuki Miyoshi 09 Sep '12

09 Sep '12

SLACS2012講演者および参加を考慮されている皆様，プログラムおよび梗概をお送り致します。京都産業大学理学部数理科学科三好博之 hxm(a)cc.kyoto-su.ac.jp ---------------------------------------------------------- 9/15（土曜日） 13:00-13:30 鴨浩靖，萩尾由貴子，溝口涼子（講演者）（奈良女子大学理学部）題目：三角形に関する平面ユークリッド幾何への数式処理の応用梗概：未定 13:35-14:05 吉村和人（JAIST）題目：オラクルの圏論的記述―終対象の一般化として―TTE (Type-2 Theory of Effectivity) は計算可能解析学の枠組みの一つである．TTEでの初等的な事実の一つとして，(計算可能性概念の導入された) ある種の位相空間の間の写像に対してはオラクル計算可能性と位相的連続性が一致するというものがある．本発表では左記事実の圏論的特徴づけについて現状得られている結果の紹介を行う．具体的には，factorization systemを伴う圏のうち適当な性質を満たすものの上で: オラクルの概念の再現; オラクル計算可能性と位相的連続性の一致に相当する命題の特徴づけ: 左記2点を吟味する． 14:10-14:40 江口直日（東北大学理学研究科）題目：Rewriting Apploaches to Computational Complexity and Complexity Analysiss by Rewriting 梗概：関数型言語により定義できる関数の多くは停止性を持つ項書き換えシステムとして表現することができる．現在まで多項式解釈，行列解釈，リダクション順序など項書き換えシステムの停止性を証明する方法が知られている．こうした停止性の証明により，しばしば停止性だけでなく時間計算量と深く関係する書き換え回数の上限を求めることができる．本講演では経路順序と呼ばれるリダクション順序による計算量解析法についてM. Avanzini, G. Moser (共に University of Innsbruck)との共同研究の成果を報告する．さらに新しく導入する経路順序は多項式時間計算量に対して完全となることを説明する． 14:40-15:00 休憩20分 15:00-15:30 河野友亮題目：論理CDの補完定理について梗概：中間論理のひとつであるCD において、クレイグの補間定理が成り立たないことが[1]によって証明された。そのおおまかな内容の解説に加え、CDを少し変えた論理でもクレイグの補間定理が成り立たないことが[1]と同様の手法で証明できることを示す。 [1] Failure of interpolation in the intuitionistic logic of constant domains, Grigori Mints, Grigory Olkhovikov, Alasdair Urquhart 15:35-16:05 岩波克（東京工業大学情報理工学研究科）題目：様相Lukasiewicz論理の公理化について梗概：Lukasiewicz論理の様相論理化にはいくつかの流儀が知られているが、最も自然と思われる、Kripke modelを用いて様相論理化したものの公理について考える。 14:40-15:00 休憩20分 16:10-16:40 龍田真（国立情報学研究所）題目：Non-Commutative First-Order Sequent Calculus 梗概：非可換一階シーケント計算NCLKについて講演する。まず、非可換 positive fragment を普通の一階シーケント計算で前件にグループがあり右交換規則のない論理体系LK-に拡張する。次のことを示す。 (1) NCLK は LJ に同等、(2) NCLKに交換規則を追加するとLKに同等になる、(3) LK-はLJに同等、(4) LK-とNCLKの間の翻訳。 16:45-17:15 龍田真（国立情報学研究所）題目：TLCA未解決問題20番: 遺伝的置換子の型梗概：TLCA未解決問題20番とは遺伝的置換子を特徴付ける型システムを見つけよという問題である．本講演はこれに答える．まず，遺伝的置換子全体が枚挙不可能であることを示すことにより，そのような型システムが存在しないことを証明する．次に，最善解として，可算無限個の型を与え，項がそのすべての型をもつこととその項が遺伝的置換子であることが同等であることを証明する．本講演はLICS2008と同じ内容である。 17:15-17:30 ビジネスミーティング（次回開催について） 18:00-20:00 懇親会 9/16（日曜日） 10:00-11:00 丸山善宏（Oxford University）題目：Duality, Quantum Symmetry and Categorical Logic 梗概：After an introduction to duality theory, this talk is two-fold while duality works as a unifying theme. In the first part, we aim at articulating Chu Duality hidden in Categorical Quantum Mechanics (i.e., dagger-compact categories), thereby giving coalgebraic and logical characterizations of quantum symmetries. In the second part, we develop the framework of Categorical Universal Logic building upon Lawvere's idea of hyperdoctrine, in which duality theory can be exploited to find various models of logic and set theory. From this perspective, we discuss the following issues: Lawvere-Tierney topology; the tripos-topos construction; and categorical quantum logic. 11:10-12:10 Nonstandard Static Analysis: Discrete Verification Methodologies 蓮尾一郎（東京大学情報理工学研究科）題目：Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications 梗概： *Hybrid systems* are those which exhibit both discrete "jump" and continuous "flow" dynamics. Their importance---as components of *cyber-physical systems*---is paramount now that more and more physical systems (cars, airplanes, etc.) are controlled with computers. There are naturally two directions towards the study of hybrid systems: *control theory* (typically continuous) and *formal verification* (typically discrete). For us from the formal verification community, therefore, the big challenge is how to incorporate continuous "flow" dynamics. Many existing techniques---such as hybrid automaton or Platzer’s differential dynamic logic---include differential equations explicitly. This incurs a difficult (and very interesting) question of how to handle differential equations. In our project we take a different path of *turning flow into jump*---more precisely into infinitely many jumps each of which is infinitesimal (i.e. infinitely small). This makes everything discrete jump dynamics, to which all the discrete techniques accumulated in the community of formal verification readily apply. This venture is mathematically supported by *nonstandard analysis*, where we can rigorously speak about infinites and infinitesimals. In the talk I will lay out: 1) our framework of a while-language and a Hoare-style program logic, augmented with an infinitesimal constant, for modeling and verification of hybrid systems; 2) how discrete verification techniques can be *transferred*, as they are, to hybrid applications, via the celebrated *transfer principle* in nonstandard analysis; and 3) the overview of our prototype automatic prover. The talk is based on the joint work with Kohei Suenaga, Kyoto University. References: [1] Kohei Suenaga and Ichiro Hasuo. Programming with Infinitesimals: A While-Language for Hybrid System Modeling. Proc. ICALP 2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag. [2] Ichiro Hasuo and Kohei Suenaga. Exercises in Nonstandard Static Analysis of Hybrid Systems. To appear in Proc. CAV 2012. 12:10-13:30 昼食 13:30-14:15 Michele Basaldella (JAIST) （この講演は英語で行われます）演題：An interactive semantics for classical arithmetic 梗概：In this talk, we introduce a sequent calculus which is a variant of some well-known proof-systems introduced by Novikoff, Tait, Coquand, and Herbelin. A common - and perhaps the most interesting - aspect of these kinds of calculi is that they can be used to provide a simple and elegant formulation of syntactical derivability for first order classical arithmetic... at a reasonable price: we have to consider infinitary formulas and infinitary derivations, rather than the usual finitary ones. In more detail, we will talk about a calculus which has the following features: * we derive sequents (finite multisets) of infinitary propositional formulas, * some inference rules may have an infinite number of premises, * derivations are infinitary trees made of sequents. We also require that both formulas and derivations are (infinitary) well-founded objects, which means that both formulas and derivations can be defined inductively. The main purpose of this talk is to define an interactive semantics for derivations strongly inspired by Girard's ludics. The target of this analysis is not the derivability predicate 'the formula A is derivable' as traditionally in logic, but the more subtle - and deeper - statement 'p is a proof of the formula A'. Specifically, we define a notion of untyped derivation and a procedure of interaction (a kind of cut-elimination procedure) between these untyped objects. Next, we we define two relations 'PROVES' and 'INTERACTIVELY' between untyped derivations 'p' and formulas 'A' such that * 'p PROVES A' is defined inductively, it corresponds to 'p is a proof of the formula A' in the sequent calculus. * 'p INTERACTIVELY A' holds whenever the interaction between 'p' and all the tests for 'A' (special derivations associated to 'A' ) terminates. We finally show a soundeness-and-completeness theorem: 'p PROVES A' if and only if 'p INTERACTIVELY A'. 14:15-15:00 木原貴行(JAIST) 題目：On some variants of the Jayne-Rogers THeorem via the Posner-Robinson Join THeorem 梗概：位相空間上の関数 F が (m,n)-可測であるとは，ボレル階層の第 m 段階に属す集合の F による逆像が常にボレル階層の第 n 段階に属すことである．20世紀初頭，ルージンは任意のボレル可測関数は可算個の連続関数に分解可能か，すなわち可算的連続かどうか尋ねた．ルージン問題は1930年代に否定的解決が与えられ，現在では，m が n 未満ならば，可算的連続でない (m,n)-可測関数が存在することが知られている．その一方，Jayne-Rogers (1984) は， (2,2)-可測性と区分的連続性が同値であることを示した． Jayne-Rogers の定理の(n,n)-可測性への拡張，乃至，ボレル可測関数の階層における可算的連続性の境界の発見は，現代の実解析学における重要な問題の一つである．本発表では，連続的(n,n)-可測性の概念を定義し，チューリング次数の代数的構造に関する Posner-Robinson Join Theorem (1981) を介して，次の 5条件の同値性を与える：「連続的 (n+1,n+1)-可測」「連続的(2,n+1)-可測かつ可算的連続」「離散ベール第 n 類」「 n 世代神託学習によって同定可能」「第 n 階区分的連続」 15:05-15:35 宮部賢志（京都大学数理解析研究所）題目：ゲーム論的確率論入門梗概：ゲーム論的確率論では測度を使わずに確率の理論を展開する．その手法はランダムネスの理論に強く影響を受けており，証明では多くの場面でアルゴリズムを作ることが要求される．そこで何らかの形でコンピュータ科学にも参考になることを期待して，ゲーム論的確率論の基本的な考え方を解説する． 15:35-15:55 休憩20分 15:55-16:40 松尾亮太（名古屋大学大学院情報科学研究科計算機数理科学専攻）題目：戦略的論理式梗概：戦略の定義を、Strategic formulaによって表現されるような写像のことと改めることによって、自然な戦略の理論の構築を目指す。R_G,n という命題論理の言語を定め、ここの論理式の内で戦略を表現するようなものをStarategic formula と呼ぶ。この枠組みによって、人が事実上用いることができる戦略の定義や、戦略の複雑さの妥当な定義が可能となる。我々の方法の応用として、ゲーム理論における最も有名な定理の一つであり、哲学的な問題点も併せ持った、The perfect folk theorem の解析を試みる。 16:45-17:30 小林聡（京都産業大学コンピュータ理工学部）題目：未定梗概：未定 17:35-18:35 佐藤雅大（名古屋大学多元数理科学研究科）題目：未定（Coqによる数学について）梗概：今回は私がCoqを用いて直観主義的集合論に基づいた数学の理論を構築したことについて発表する。Coqで集合論を展開するという試みはたくさん存在するが、今回は「Coqで集合論を展開した」ということより「Coqで展開できた集合論の上でどのように数学が展開できたか」という点に焦点を置いて発表したい。 18:35-18:40 次回予定アナウンスおよび挨拶

1 0

SLACS2012参加案内およびプログラム（9/9 ver.）
by Hiroyuki Miyoshi 09 Sep '12

09 Sep '12

SLACS2012講演者の方々および参加者を考慮されている皆様， 9/15-16に開催されるSLACS2012の参加案内およびプログラムの 9/9 ver.をお送りします。前回との変更点は以下の通りです。 * 司会のことを考慮して9/16の蓮尾一郎さん，丸山善宏さん， Michele Basaldellaさんの順序を変更しました。もしご都合が悪ければご連絡をよろしくお願いいたします。 * 蓮尾一郎さん，小林聡さん，佐藤雅大の講演時間短縮をなくしました。既に研究会直前ですので前回のアナウンス通りに 15分以上短縮されても昼食や終了が前倒しになるだけで大丈夫なようにしてあります。講演予定に合わせてお決め下さい。 * 懇親会の時間を30分繰り上げました。 ---------------------------------------------------------- SLACS2012研究会への参加案内第29回記号論理と情報科学研究集会 (SLACS 2012) は，京都産業大学むすびわざ館で開催の予定です．SLACSは，記号論理学とコンピュータ科学の研究者や学生の相互交流を目的として開催されている研究集会で毎年持ち回りで行われています（http://www.math.s.chiba-u.ac.jp/SLACS/）。完成された研究のみならず，発展途上の話題やサーベイなども大歓迎です．記号論理以外にも，圏論やアルゴリズム理論などコンピュータ科学に関わるご講演を広く行われます。開催要項開催日：2011年9月15日（土）13:00 〜 9月16日（日）18:20 場所：京都産業大学むすびわざ館〒600-8533 京都市下京区中堂寺命婦町1-10 Tel.075-277-1600　Fax.075-277-1699 （京都産業大学神山キャンパスとは異なります） http://www.kyoto-su.ac.jp/outline/shisetsu/musubiwaza/ アクセス：最寄り駅はJR丹波口駅および阪急大宮駅 http://www.kyoto-su.ac.jp/outline/shisetsu/musubiwaza/access.html 研究会参加について申し込みも費用も不要です（懇親会については後述）。皆様ふるってご参加よろしくお願いいたします。懇親会は9月15日18:00-20:00に予定しています．かごの屋五条七本松店 075-326-1165 http://www.kinrei.com/shop/spec/?shop_id=42 http://r.gnavi.co.jp/k539974/ （ぐるなび）懇親会の参加・不参加についても事前に連絡して頂けると助かります。（9/15の15:00頃に人数を確定して私が店に連絡致します。予算3-4千円程度）。梗概については長くなりますので別のメールでお送り致します。現在まだ，題目・梗概が未定の方は連絡をよろしくお願い致します。 ---- 京都産業大が理学部数理科学科三好博之 hxm(a)cc.kyoto-su.ac.jp ---------------------------------------------------------- SLACS2012 プログラム 9/15（土曜日） 13:00-13:30 三角形に関する平面ユークリッド幾何への数式処理の応用鴨浩靖，萩尾由貴子，溝口涼子（講演者）（奈良女子大学理学部） 13:35-14:05 オラクルの圏論的記述―終対象の一般化として― 吉村和人（JAIST） 14:10-14:40 Rewriting Apploaches to Computational Complexity and Complexity 江口直日（東北大学理学研究科） 14:40-15:00 休憩20分 15:00-15:30 論理CDの補完定理について河野友亮（東京工業大学情報理工学研究科） 15:35-16:05 様相Lukasiewicz論理の公理化について岩波克（東京工業大学情報理工学研究科） 14:40-15:00 休憩20分 16:10-16:40 Non-Commutative First-Order Sequent Calculus 龍田真（国立情報学研究所） 16:45-17:15 TLCA未解決問題20番: 遺伝的置換子の型龍田真（国立情報学研究所） 17:15-17:30 ビジネスミーティング（次回開催について） 18:00-20:00 懇親会 9/16（日曜日） 10:00-11:00 Duality, Quantum Symmetry and Categorical Logic 丸山善宏（Oxford University） 11:10-12:10 Nonstandard Static Analysis: Discrete Verification Methodologies 蓮尾一郎（東京大学情報理工学研究科） 12:10-13:30 昼食 13:30-14:15 An interactive semantics for classical arithmetic (in English) Michele Basaldella (JAIST) 14:15-15:00 On some variants of the Jayne-Rogers THeorem via the 木原貴行(JAIST) 15:05-15:35 ゲーム論的確率論入門宮部賢志（京都大学数理解析研究所） 15:35-15:55 休憩20分 15:55-16:40 戦略的論理式松尾亮太（名古屋大学大学院情報科学研究科計算機数理科学専攻） 16:45-17:30 未定小林聡（京都産業大学コンピュータ理工学部） 17:35-18:35 未定（Coqによる数学について）佐藤雅大（名古屋大学多元数理科学研究科） 18:35-18:40 次回予定アナウンスおよび挨拶 ----

1 0

CAPEロジック・ワークショップのお知らせ
by 矢田部俊介 07 Sep '12

07 Sep '12

# 複数受け取られた場合はご容赦ください。今月9月18日（火）の 10時30分〜17時に、京都大学文学部校舎二階第六講義室において、CAPEロジック・ワークショップのご案内をご転送いたします。皆様のご参加をお待ち申し上げます。矢田部俊介 --------- 皆様京都大学文学研究科附属応用哲学・倫理学教育研究センター（CAPE）の主催にて、 CAPEロジック・ワークショップが下記のように開催されます。皆様のご参加をお待ち申し上げます。京都大学大学院文学研究科附属応用哲学・倫理学教育研究センター http://www.bun.kyoto-u.ac.jp/cape/cape-top_page/ 事務補佐　　竹中利彦〒606-0085 京都市左京区吉田本町　京都大学文学部内 CAPE(a)bun.kyoto-u.ac.jp --- 記 --- CAPEロジック・ワークショップ日時：2012年9月18日（火） 10時30分〜17時場所：文学部校舎二階第六講義室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm （8番の建物です）講演者・題目： 10:30-12:00 大西琢朗　 "Usefulness of deduction and Proof-Theoretic Semantics" 13:30-15:00 Shawn Standefer: "Truth and conditionals" 15:30-17:00 丸山善宏 "Categorical Harmony and Degrees of Paradoxity" **************************************************************************** ********** CAPE Logic workshop Date : September 18 (Tuesday) Place:　 The 6th lecture room, 2nd floor, Faculty of letters, Kyoto University (building no.6 of the following map) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm *Schedule: 10:30-12:00 Takuro Onishi: "Usefulness of deduction and Proof-Theoretic Semantics" 13:30-15:00 Shawn Standefer: "Truth and conditionals" 15:30-17:00 Yoshihiro Maruyama: "Categorical Harmony and Degrees of Paradoxity" *Abstracts (1)Speaker: Takuro Onishi Title: Usefulness of deduction and Proof-Theoretic Semantics Abstract: Michael Dummett’s anti-realist theory of meaning is considered to provide a philosophical basis of proof-theoretic semantics, which is an inferentialis approach to logical validity. Unfortunately, in the debate of proof-theoretic semantics, due attention has not been paid to his fundamental consideration on the nature of deductive inference, in which he emphasizes its usefulness or fruitfulness as well as its validity. That is, deduction is a special kind of activity of extending our knowledge. Dummett represents it as involving a certain tension between validity and usefulness, and tries to reconcile it against the background of his own meaning theory. In this talk I present Dummett’s view on deduction, and compare it with G.Restall’s bilateralist explication of logical consequence which would justify classical logic. (2)Speaker: Shawn Standefer Title: Truth and conditionals Abstract: Some recent approaches to truth have adopted the strategy of enriching the underlying logic with a new conditional. I will provide some background on these approaches and distinguish different roles that such conditionals play in the theory. I will show how this distinction plays out in an extension of the revision theory of truth and use the distinction to offer a philosophical defense of that theory. (3)Speaker: Yoshihiro Maruyama Title: Categorical Harmony and Degrees of Paradoxity Abstract: Prior's weird connective "tonk" compelled logicians to articulate the concept of a logical constant, eventually giving rise to developments of proof-theoretic semantics in the spirit of inferentialism, and to the notion of proof-theoretic harmony in particular, which works as a criterion to judge if a connective is a proper logical constant or not. Different concepts of harmony have been proposed and discussed by Belnap, Dummett, and many others. Building upon Lawvere's understanding of logic via category theory, I formulate a categorical concept of harmony relativised to primitive vocabulary, and compare it with other notions of harmony. The categorical conception of harmony leads us to a novel analysis of the nature of tonk: namely, the problem of tonk is the problem of equivocation in terms of adjoint functors. It finally turns out that there are different degrees of paradoxity of logical constants from a categorical perspective. All slot consist of 60 minutes talk and 30 minutes discussion.

1 0

研究集会案内：証明論と複雑性
by Suzuki Toshio 07 Sep '12

07 Sep '12

　研究集会案内（複数お受け取りの場合はご容赦ください）首都大学東京の鈴木登志雄です。以下の研究集会に多数の講演・参加申込みをありがとうございます。参加申込みをされていない方の当日参加も歓迎しますので、お気軽にお越しください。 ------------------------------------------------------------------ ＲＩＭＳ研究集会「証明論と複雑性（Proof theory and complexity）」期間　２０１２年９月１２日（水）午後から１４日（金）午後場所　京都大学数理解析研究所４２０号室 http://www.ac.auone-net.jp/~bellp/meeting/proof2012.html ------------------------------------------------------------------ 講演プログラムは上記サイトに掲載してあります。 -- 鈴木登志雄首都大学東京理工学研究科数理情報科学専攻 toshio-suzuki [atmark] tmu.ac.jp

1 0

第15回プログラミングおよびプログラミング言語ワークショップ(PPL2013)ご案内
by Yoshinori Tanabe 07 Sep '12

07 Sep '12

(重複の場合はご容赦ください．メール送信は田辺@NIIが行っています．) 東京工業大学の権藤と京都大学の勝股と申します．来年3月に福島県会津若松東山温泉で開催される第15回プログラミングおよびプログラミング言語ワークショップ (PPL2013) のご案内です．詳細な投稿方法などは決定次第，下記ワークショップwebページにてお知らせしますので，ご投稿，ご参加をご検討ください． -------------------------------------------------------------------------- 第15回プログラミングおよびプログラミング言語ワークショップ（PPL2013） http://www.pllab.riec.tohoku.ac.jp/ppl2013/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2013年3月4日(月)〜3月6日(水) 会場: 福島県会津若松東山温泉「御宿東鳳」http://www.onyado-toho.co.jp/ PPL2013は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表（既発表・未発表の別を問いません） ※ショートプレゼンテーションは行いませんカテゴリ１の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また，ポスター・デモを含む全発表のなかから，聴衆の投票により，最も優秀なプレゼンテーションに発表賞（一般の部，学生の部）を授与する予定です．カテゴリ１（国内外未発表論文） ------------------------------ 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です（ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません）．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとする予定です．採録された論文は，PPL2013参加者に配布される予稿集に掲載され，参加者のみがアクセス可能な形でWEB上で公開されます（論文へのリンク集ページを作成し，閲覧に必要なパスワードを参加者に連絡します）．カテゴリ１で発表された研究のうち，PPL2013プログラム委員会として優れていると認めるものは，PPL2013終了後（2013年4月下旬予定），「コンピュータソフトウェア」誌PPL2013推薦論文としての投稿が可能です．推薦論文は，PPL プログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ２（国外既発表論文） ---------------------------- 査読付の国際会議または学術雑誌等で既発表であるが，国内では未発表な研究の紹介をする場です．採録決定済みの研究も含みます．PPLへの関連をもとに採録を判定いたします．カテゴリ３（ポスター・デモ発表） ------------------------------------------ ２時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また，申込多数の場合は抽選によって採否を決定する可能性があります．なお，PPL2013 ではポスターやデモによる活発な意見交換を促進したいという観点から，ショートプレゼンテーションのセッションは設けません． ====================================================================== 投稿・発表申込要領３つのカテゴリそれぞれに対して，投稿は以下のように行って下さい．最新の情報は上記Webページでご確認下さい．カテゴリ１（国内外未発表論文） ------------------------------ 投稿手続きは二段階です．発表申込を行った上で論文提出を行って下さい．発表申込先： EasyChair による申し込みを予定しています．発表申込締切：2012年12月21日(金) 17:00 (JST) 著者名，所属，論文タイトル，論文概要（日本語300〜400字程度もしくは英語200 words程度）を提出してください．論文提出締切：2013年1月11日(金) 17:00 (JST) 10ページ程度（最大15ページ）の論文（英語もしくは日本語，PDF形式）を提出して下さい．採否通知：2013年2月4日(月) 最終原稿提出締切：2013年2月15日(金) 17:00 (JST) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします． (注) カテゴリ１への投稿論文と類似の論文を，他の会議（予稿集を出版するもの）・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記して下さい．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります（他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります）．カテゴリ２（国外既発表論文） ---------------------------- 昨年同様，カテゴリ2の申込締切が少し早くなっていますのでご注意ください．発表申込時に採録が決定している国際会議または学術雑誌等の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込先： submit-ppl2013 [at] kurims.kyoto-u.ac.jp （[at]を@に置き換えて下さい）発表申込締切：2013年1月23日(水) 17:00 (JST) 原論文（ページ数不問，PDF形式）とabstract（テキスト形式）を，著者名，所属，論文タイトル，原論文の出典（発表会議名，掲載済／予定の別等）と併せて上記申込先宛にお送り下さい．採否通知：2013年2月4日(月) 最終原稿提出締切：2013年2月15日(金) 17:00 (JST) カテゴリ３（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行なわずに募集いたします．デモを行なう場合は，発表概要においてその旨をご説明ください．発表申込先： submit-ppl2013 [at] kurims.kyoto-u.ac.jp （[at]を@に置き換えて下さい）発表申込締切：2013年2月6日(水) 17:00 (JST) 著者名，所属，発表タイトル，発表概要（200〜300字程度），希望する発表形態（ポスター・デモの別），をテキスト形式で上記申込先宛にお送り下さい．採否通知：2013年2月15日(金) 問い合わせ先：oc-ppl2013 [at] kurims.kyoto-u.ac.jp （[at]を@に置き換えて下さい） ====================================================================== プログラム委員会青木利晃 (北陸先端科学技術大学院大学) 青谷知幸 (北陸先端科学技術大学院大学) 天野俊一 (IBM東京基礎研究所) 磯部祥尚 (産業技術総合研究所) 岩見宗弘 (島根大学) 角谷良彦 (東京大学) 勝股審也 (京都大学) [プログラム共同委員長] 小宮常康 (電気通信大学) 権藤克彦 (東京工業大学) [プログラム共同委員長] 田浦健次朗 (東京大学) 高田喜朗 (高知工科大学) 田辺良則 (国立情報学研究所) 中田景子 (Institute of Cybernetics at Tallinn University of Technology) 中野圭介 (電気通信大学) 長谷部浩二 (筑波大学) 番原睦則 (神戸大学) 松崎公紀 (高知工科大学) 実行委員会上野雄大 (東北大学電気通信研究所) [実行委員長] 鵜川始陽 (電気通信大学) [実行副委員長] 勝股審也 (京都大学) [プログラム共同委員長] 権藤克彦 (東京工業大学) [プログラム共同委員長] -------------------------------------------------------------------------- 田辺良則国立情報学研究所 GRACEセンター y-tanabe(a)nii.ac.jp

1 0

APLAS 2012: Call for Posters and Demos
by Kohei SUENAGA 07 Sep '12

07 Sep '12

# 複数受け取られた場合はご容赦ください。京都大学の末永幸平と申します。 12月11〜13日に京都で開催される APLAS 2012 のポスター・デモ募集のお知らせをお送りします。今年の APLAS はせっかくの国内開催ですので、多数のご発表をお待ち申し上げております。末永幸平京都大学白眉センター ksuenaga(a)fos.kuis.kyoto-u.ac.jp -- 10th Asian Symposium on Programming Languages and Systems (APLAS 2012) Call for Poster and Demos APLAS 2012 will include a poster and demo session during the conference. The poster session aims to give students and professionals an opportunity to present technical materials to the research community, and to get responses from other researchers in the field. This year, accepted posters will be presented in the main hall so that presenters have much opportunity of discussion during breaks. Standing by the poster on each break is not mandatory, though. * Scope Poster and demo contributions are sought in all areas of programming languages and systems, including the following topics: - semantics, logics, foundational theory; - design of languages and foundational calculi; - type systems; - compilers, interpreters, abstract machines; - program derivation and transformation; - program analysis, verification, model-checking, software security; - concurrency, constraints, domain-specific languages; - tools for programming, verification, implementation. * Format of Posters A space of A1 paper size (594 mm wide and 841 mm high) will be provided for each presentation. AC Power outlet of 100V will be also provided during the poster & demo session. If you need more space and facilities, contact the poster chair (aplas2012-poster AT fos.kuis.kyoto-u.ac.jp). * Submission Each presenter should e-mail a 1-2 page abstract in PDF to the poster chair (Kohei Suenaga: aplas2012-poster AT fos.kuis.kyoto-u.ac.jp) by October 5th 2012. The abstract should include the title, author(s), affiliation(s) and summary of the work. The program of the poster session will be announced by October 29th, 2012. We hope to accommodate every poster, but may restrict presentations (based on relevance and interest to the community) due to space constraints. * Important Dates Submission deadline: October 5th, 2012 Notification: October 29th, 2012 * Contact Poster chair: Kohei Suenaga (aplas2012-poster AT fos.kuis.kyoto-u.ac.jp)

1 0

SLACS 2012 Program　(9/6 ver.）
by Hiroyuki Miyoshi 07 Sep '12

07 Sep '12

SLACS 2012講演者・参加者の皆様， SLACS 2012について予想以上にたくさんの講演申し込みがありました。どうもありがとうございます。とりあえず暫定版のプログラムをお送り致します。梗概については後ほど別便でお送り致します。講演数が多くプログラムがかなりタイトになっていますがご容赦下さい。(*)印の方は講演時間の多少の短縮をお願い致したく思います。講演者で日程等ご都合の悪い方はお知らせ下さい。また，申し込んだはずなのにプログラムに名前がないという方も至急お知らせ下さい。現在最終日の撤収について事務と交渉中なので多少プログラムが変わることがあります。講演者でまだ題目・梗概が未定の方は連絡をよろしくお願いします。また参加には申し込みは必要ありませんが，懇親会に参加される予定の方については事前に連絡して頂けるとおおまかな人数の把握に助かりますのでご協力頂けると助かります。（9/15の15:00頃に人数を確定して店に連絡致します。予算3-4千円程度）。三好博之 ---- 9/15（土曜日） 13:00-13:30 三角形に関する平面ユークリッド幾何への数式処理の応用鴨浩靖，萩尾由貴子，溝口涼子（講演者）（奈良女子大学理学部） 13:35-14:05 未定吉村和人（JAIST） 14:10-14:40 Rewriting Apploaches to Computational Complexity and Complexity 江口直日（東北大学理学研究科） 14:40-15:00 休憩20分 15:00-15:30 論理CDの補完定理について河野友亮（東京工業大学情報理工学研究科） 15:35-16:05 未定岩波克（東京工業大学情報理工学研究科） 14:40-15:00 休憩20分 16:10-16:40 Non-Commutative First-Order Sequent Calculus 龍田真（国立情報学研究所） 16:45-17:15 TLCA未解決問題20番: 遺伝的置換子の型龍田真（国立情報学研究所） 18:00-20:00 懇親会 9/16（日曜日） 10:00-10:45 An interactive semantics for classical arithmetic (in English) Michele Basaldella (JAIST) 10:50-11:50 Duality, Quantum Symmetry and Categorical Logic 丸山善宏（Oxford University） 11:50-13:20 昼食 13:20-14:10 Nonstandard Static Analysis: Discrete Verification Methodologies 蓮尾一郎（東京大学情報理工学研究科）(*) 14:15-15:00 On some variants of the Jayne-Rogers THeorem via the 木原貴行(JAIST) 15:05-15:35 ゲーム論的確率論入門宮部賢志（京都大学数理解析研究所） 15:35-15:55 休憩20分 15:55-16:40 自然な戦略の理論松尾亮太（名古屋大学多元数理科学研究科） 16:45-17:15 未定小林聡（京都産業大学コンピュータ理工学部）(*) 17:20-18:10 未定（Coqによる数学について）佐藤雅大（名古屋大学多元数理科学研究科）(*) 18:10-18:30 ビジネスアナウンスメント（次回開催について）撤収

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml