- Logic-ml - fos.kuis.kyoto-u.ac.jp

Talk by Jean-Yves Girard at RIMS, Kyoto U. (1/12)
by Kazushige TERUI 09 Jan '12

09 Jan '12

みなさま今週木曜日に催されるセミナーのご案内をさせていただきます。どうぞお気軽にお越しください。照井 --- RIMS-CS website http://www.kurims.kyoto-u.ac.jp/~cs/ ===== Speaker: Jean-Yves Girard (IML Marseille & RIMS Kyoto) Title: A SECOND LOOK AT PROOF-NETS Date: 11.00 -, January 12th (Thu) Place: Room 478, "Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan)" http://www.kyoto-u.ac.jp/en/access/campus/main.htm (Next to our CS Lab) 総合研究2号館 478号室 (CS室のとなりです) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm Abstract: In logic, we have a reasonable answer to the question : "What is a typable object?" but none so far to the question : "What is a typed object?" By a second look at proof-nets, especially the ones involving quantifiers, we shall propose an answer to the second question. ------------------------------------------ Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui(a)kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/

1 0

情報処理学会第88回プログラミング研究発表会(2012/03) 発表募集 (再送)
by Keisuke Nakano 06 Jan '12

06 Jan '12

＊＊＊＊複数受け取られた方はご容赦ください＊＊＊＊電気通信大学の中野と申します． 3月に産業技術総合研究所つくばセンターにて開催予定の，情報処理学会第88回プログラミング研究会の発表申込締切（ 1月13日(金) ）が迫ってまいりました．発表募集のご案内を再送いたしますので，投稿・発表についてどうぞご検討ください．申込時点で必要なのはタイトルと概要などです． http://www.ipsj.or.jp/sig/pro/trans-author.html -- 中野圭介 / Keisuke Nakano この場を借りて2011年度第5回情報処理学会プログラミング研究発表会の発表募集のご案内をさせて頂きたく存じます．プログラミング研究会(PRO)は，・プログラミング言語の設計，処理系の実装・プログラミングの理論，基本概念・プログラミング環境，支援システム・プログラミング方法論，パラダイム・これらを応用したシステムの開発事例・その他，プログラミングに関する面白い話題を対象とした研究発表の場で，1998年度から毎年3-4回のペースで論文誌を発行しています．PRO論文誌は研究会と密接にリンクしており，研究会で発表されたもののうちあらかじめ論文投稿を希望し，論文原稿を提出されているものが査読の対象となっています (論文誌投稿を希望しない発表も歓迎します)．おおむね研究会から3週間で論文の採否が決定されるという迅速さも大きな特徴です． 2012年3月の研究会も多くの発表ならびに論文投稿をお待ちしております．参加費は無料です．申込締切は1月13日(投稿締切は2月13日)ですので，よろしくご検討ください．なお，多数の発表申込みがある場合には，発表をお断りすることがございますので，お早めにお申し込みください．また，今回も和文として投稿された論文の英語化を支援する試みを実施します．和文原稿にて採録を判断し，(著者が希望する場合は) 採録決定後に英語化していただいてから掲載致します．この英語化に関する詳細については， http://millsmess.cs.uec.ac.jp/pro/2011-5/english-paper-encouragement.html をご覧ください．第88回プログラミング研究会(PRO-2011-5)発表募集日程: 2012年3月15日(木)・16日(金) 会場: 産業技術総合研究所つくば中央共用講堂中会議室〒305-8561　茨城県つくば市東1-1-1　中央第1 つくばエクスプレス線つくば駅からバス約20分 (交通ガイド: http://www.aist.go.jp/aist_j/guidemap/tsukuba/center/tsukuba_map_c.html) 発表申込締切: 2012年1月13日(金) 投稿論文原稿提出締切: 2012年2月13日(月) 申込先: 中野圭介(電通大) E-mail: ksk [at] cs.uec.ac.jp 案内ページ: http://millsmess.cs.uec.ac.jp/pro/2011-5/ ・申込みに当たっての注意はプログラミング研究会のページ http://www.ipsj.or.jp/sig/pro/ を参照してください．・できるだけE-mailでお願いします．・申込み後返信がない場合はご連絡下さい．

1 0

Prof. Kwangkeun Yi Lecture at NII Logic Seminar
by Makoto Tatsuta 04 Jan '12

04 Jan '12

Prof. Kwangkeun Yi Lecture at NII Logic Seminar Date: January 10, 2012, 15:00--17:00 Place: National Institute of Informatics, Lecture Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/introduce/access1-j.shtml) Speaker: Prof. Kwangkeun Yi (Seoul National University) Title: Static Analysis of Multi-Staged Programs via Unstaging Translation Abstract: Static analysis of multi-staged programs is challenging because the basic assumption of conventional static analysis no longer holds: the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. This article presents a semantic-preserving translation of multi-staged call-by-value programs into unstaged programs and a static analysis framework based on this translation. The translation is semantic-preserving in that every small-step reduction of a multi-staged program is simulated by the evaluation of its unstaged version. Thanks to this translation we can analyze multi-staged programs with existing static analysis techniques that have been developed for conventional unstaged programs: we first apply the unstaging translation, then we apply conventional static analysis to the unstaged version, and finally we cast the analysis results back in terms of the original staged program. Our translation handles staging constructs that have been evolved to be useful in practice (typified in Lisp's quasi-quotation): open code as values, unrestricted operations on references and intentional variable-capturing substitutions. This article omits references for which we refer the reader to our companion technical report. This is a joint work with Wontae Choi, Baris Aktemur, and Makoto Tatsuta. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

Nagoya set theory seminar
by 吉信康夫 20 Dec '11

20 Dec '11

(重複して受け取られた場合はご容赦ください) 名古屋集合論セミナーのご案内：日時：2012年1月11日(水) 午後2時15分～4時(途中15分休憩) 場所：名古屋大学大学院情報科学研究科棟 322号室 (名古屋市地下鉄名城線名古屋大学駅1番出口より徒歩数分、下記のキャンパスマップのA4にある建物です。) http://www.nagoya-u.ac.jp/global-info/access-map/higashiyama/ 講演者：Franklin D. Tall (トロント大学) 題目：A useful model of set theory アブストラクト: I will sketch a method for getting mutually consistent consequences of PFA and V = L. The talks are unavoidably technical, and assume acquaintance with the method of proper forcing with elementary submodels as side conditions. The hope is that although listeners are unlikely to be able to follow all the details presented, they will get enough of the ideas so that they can more easily study the research papers if they are interested. 多数のご参加をお待ちしております。名古屋大学大学院情報科学研究科吉信康夫

1 0

Fwd: [Proof Complexity] Postdoc position in proof complexity at KTH
by Satoru Kuroda 20 Dec '11

20 Dec '11

logic-ml の皆様，黒田＠群馬県立女子大学です． Proof complexity の ML にポスドク募集の案内が流れてきましたので，こちらに流します．すでにご覧になっている場合はご容赦ください． ---------- Forwarded message ---------- From: Jakob Nordstrom <jakobn(a)kth.se> Date: 2011/12/20 Subject: [Proof Complexity] Postdoc position in proof complexity at KTH To: proof-complexity(a)math.cas.cz Dear colleagues, This is just to ask for your help in advertising an open postdoc position in proof complexity at KTH Royal Institute of Technology. The formal deadline is January 31, but candidates are encouraged to apply already now. The intended start date is August-September 2012. I would be very grateful if you could help spread this information. For more details, see the enclosed PDF flyer, which is also available at http://www.csc.kth.se/~jakobn/openings/PostdocAug12Flyer.pdf . The full, formal announcement can be found at http://www.csc.kth.se/~jakobn/openings/D-2011-0603-Eng.php . As advertised before on this list, I am also looking for two PhD students, and here the formal announcement is http://www.csc.kth.se/~jakobn/openings/D-2011-0503-Eng.php . Informal enquiries about the postdoc or PhD positions are welcome. With best regards, Jakob Nordstrom Jakob Nordström, Assistant Professor KTH Royal Institute of Technology Osquars backe 2, SE-100 44 Stockholm, Sweden Phone: +46 8 790 69 19 (office), +46 70 742 21 98 (cell) http://www.csc.kth.se/~jakobn/ _______________________________________________ Proof-Complexity mailing list Proof-Complexity(a)math.cas.cz http://list.math.cas.cz/listinfo/proof-complexity -- Satoru Kuroda Gunma Prefectural Women's University

1 0

Fwd: categories: MSFP 2012 deadline extension
by Ichiro Hasuo 18 Dec '11

18 Dec '11

Dear colleagues, The deadline for MSFP 2012 has been extended by one week to FRIDAY 23 DECEMBER. See details below. Best regards, James Chapman and Paul Blain Levy MSFP 2012 co-chairs -- Fourth Workshop on MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING 25 March, Tallinn, Estonia A satellite workshop of ETAPS 2012 http://cs.ioc.ee/msfp/msfp2012/ The fourth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? Type theory without universes? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control. The first MSFP workshop was held in Kuressaare, Estonia, in July 2006, affiliated with MPC 2006 and AMAST 2006. The second MSFP workshop was held in Reykjavik, Iceland as part of ICALP 2008. The third MSFP workshop was held in Baltimore, USA, as part of ICFP 2010. Important Dates: ================ Submission of papers: 23 December 2011 Notification: 25 January 2012 Final versions due: 6 Feburary 2012 Workshop: 25 March 2012 Invited Speakers: ================= Danko Ilik, Goce Delčev University of Štip, Republic of Macedonia Neil Ghani, University of Strathclyde, UK Submission: =========== Papers must report previously unpublished work and not be submitted concurrently to another conference with refereed proceedings. Accepted papers must be presented at the workshop by one of the authors. There is no specific page limit, but authors should strive for brevity. Accepted regular papers will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). After the workshop, there might be an opportunity to publish selected papers in a journal special issue. All submissions must be in PDF format and use the EPTCS style files. Submissions can be made through the EasyChair website, at http://www.easychair.org/conferences/?conf=msfp2012 ETAPS: ====== European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of six main annual conferences (one of them, POST, being new in 2012), accompanied by satellite workshops. ETAPS 2012 is the fifteenth event in the series. http://www.etaps.org/2012 Host City: ========== Tallinn, a city of 412,000 people, is the capital and largest city of Estonia, a small EU member country in Northern Europe, bordering Russia to the East and Latvia to the south. Located in the north of the country, on the southern shores of the Gulf of Finland, opposite Helsinki in Finland, Tallinn is most well known for its picturesque medieval Old Town, a UNESCO World Heritage site. But it also has a vivid cultural scene, outperforming most European centres of similar size. In 2011, Tallinn, along with Turku in Finland, is the Cultural Capital of Europe. Tallinn is easy to travel to. Estonia is part of Schengen and the Eurozone. The Lennart Meri International Airport of Tallinn /TLL) is only 4km from the city centre. Programme Committee: ==================== * James Chapman (co-chair), Institute of Cybernetics, Tallinn, Estonia * Paul Blain Levy (co-chair), University of Birmingham, UK * Thorsten Altenkirch, University of Nottingham, UK * Robert Atkey, University of Strathclyde, Glasgow, UK * Nils Anders Danielsson, Chalmers University and University of Gothenburg, Sweden * Martin Escardo, University of Birmingham, UK * Ichiro Hasuo, University of Tokyo, Japan * Ralf Hinze, University of Oxford, UK * Neelakantan Krishnaswami, Microsoft Research, Cambridge, UK * Daniel R. Licata, Carnegie Mellon University, Pittsburgh, PA * Ulrich Schoepp, LMU Munich, Germany * Alex Simpson, University of Edinburgh, UK * Matthieu Sozeau, INRIA, Paris, France * Sam Staton, University of Cambridge, UK Further Information: ==================== For more information about the workshop, go to: http://cs.ioc.ee/msfp/msfp2012/ With any other questions please do not hesitate to contact the co-chairs at msfp2012(a)easychair.org. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Logic, Algebra, and Truth Degrees 2012 - First Call
by latd12＠jaist.ac.jp 14 Dec '11

14 Dec '11

Logic, Algebra and Truth Degrees 2012 http://www.jaist.ac.jp/rcis/latd12/ First Call for Papers The third official meeting of the EUSFLAT Working Group on Mathematical Fuzzy Logic [1] will be held on 10-14 September 2012 in Kanazawa, Japan. The conference is organized by Research Center for Integrated Science [2], Japan Advanced Institute of Science and Technology [3]. Mathematical Fuzzy Logic is a subdiscipline of Mathematical Logic which studies the notion of comparative truth. The assumption that 'truth comes in degrees' has proved to be very useful in many, both theoretical and applied, areas of Mathematics, Computer Science and Philosophy. The main goal of this meeting is to foster collaboration between researchers in the area of Mathematical Fuzzy Logic, and to promote communication and cooperation with members of neighbouring fields. The featured topics include, but are not limited to, the following: . Proof systems for fuzzy logics: Hilbert, Gentzen, natural deduction, tableaux, resolution, computational complexity, etc. . Algebraic semantics: residuated lattices, MTL-algebras, BL-algebras, MV-algebras, Abstract Algebraic Logic, functional representation, etc. . Game-theory: Giles games, Rényi-Ulam games, evaluation games, etc. . First-order fuzzy logics: axiomatizations, arithmetical hierarchy, model theory, etc. . Higher-order fuzzy logical systems: type theories, Fuzzy Class Theory, and formal fuzzy mathematics. . Philosophical issues: connections with vagueness and uncertainty. . Applied fuzzy logical calculi: foundations of logical programming, logic-based reasoning about similarity, description logics, etc. We also welcome contributions on any relevant aspects of related logical systems (such as substructural and quantum logics, and many-valued logics in general). Conference Web Site: http://www.jaist.ac.jp/rcis/latd12/ Important dates: . 22 April 2012: deadline for submissions . 3 June 2012: notifications sent . 10-14 September 2012: conference Programme Committee: . Stefano Aguzzoli (University of Milano, Italy) . Matthias Baaz (Vienna University of Technology, Austria) . Petr Cintula (Academy of Sciences, Czech Republic) . Carles Noguera (CSIC, Spain) . Hiroakira Ono (JAIST, Japan), Chair . James Raftery (University of KwaZulu-Natal, South Africa) . Constantine Tsinakis (Vanderbilt University, USA) Invited Speakers: . Rostislav Horčík (Academy of Sciences, Czech Republic) . Emil Jeřábek (Academy of Sciences, Czech Republic) . Daniele Mundici (University of Florence, Italy) . Greg Restall (University of Melbourne, Australia) . Luca Spada (University of Salerno, Italy) Tutorial: . Felix Bou (University of Barcelona, Spain) If you are interested in presenting a paper, please submit a 2–4 pages abstract at http://www.easychair.org/conferences/?conf=latd2012 Your submission will be confirmed automatically on the e-mail address you provide. The accepted abstracts will be available on-line after the final decision of the program committee. If you have any problems to submit an abstract, please contact us at mail to: latd2012(a)jaist.ac.jp The deadline for contributions is 22 April 2012. The notification of acceptance/rejection will be sent until 3 June 2012. Conference dates: The scientific program will start Monday morning (10 September) and finish Friday noon (14 September). Wednesday afternoon we plan an excursion. Venue: The conference will be held in the city of Kanazawa [4,5,6], located in the Ishikawa prefecture of Japan on the Japan Sea. The venue is the Ishikawa Prefectural Museum of Art [7] in the center of Kanazawa. Local Organizing Committee: . Norbert Preining (JAIST, Japan), Chair . Katsuhiko Sano (JAIST, Japan) . Kazushige Terui (Kyoto University, Japan) . Shunsuke Yatabe (AIST, Japan) For further information please contact: latd2012(a)jaist.ac.jp [1] http://www.mathfuzzlog.org/ [2] http://www.jaist.ac.jp/rcis/en/ [3] http://www.jaist.ac.jp/ [4] http://en.wikipedia.org/wiki/Kanazawa,_Ishikawa [5] http://www.kanazawa-tourism.com/ [6] http://wikitravel.org/en/Kanazawa [7] http://www.ishibi.pref.ishikawa.jp/index_j.html

1 0

東北大学ロジックセミナーのご案内(12月26日)
by Naohi Eguchi 08 Dec '11

08 Dec '11

(本案内を重複してお受け取りの際はご容赦ください) Logic-ml の皆様，東北大学の江口と申します．下記の要領で東北大学ロジックセミナー(田中一之研究室)を開催いたします．興味のある方は参加をご検討ください．日時：12月26日(月)，16時から．場所：東北大学北青葉山キャンパス理学総合棟1201号室発表者：新井敏康 (千葉大学大学院理学研究科) タイトル：Searching witnesses of $\Sigma^{0}_{2}$-formulas in proofs アブストラクト： We can find a witness of a PA-provable $\Sigma^{0}_{2}$-formula as limits of an elementary recursive function, whose convergence is ensured by weakly descending chains of ordinals. 東北大学ロジックセミナーの詳細につきましては下記をご参照ください． https://sites.google.com/site/sendailogichomepage/ -- 江口直日東北大学大学院理学研究科数学専攻産学官連携研究員 980-8578 宮城県仙台市青葉区荒巻字青葉6ー3 E-mail: eguchi(a)math.tohoku.ac.jp

1 0

PPL2012論文募集
by Koji Nakazawa 07 Dec '11

07 Dec '11

（重複の場合はご容赦ください．）京都大学の中澤です．来年3月に和歌山県白浜温泉で開催される第14回プログラミングおよびプログラミング言語ワークショップ (PPL2012) のご案内（2回目）です．みなさまのご投稿，ご参加をお待ちしております．論文投稿・発表申込方法の詳細と招待講演者の情報を追加いたしました．カテゴリ1はeasy chairを通して，カテゴリ2, 3は下記投稿用メールアドレスまでお申込ください．最新情報は引き続き下記ワークショップwebページにてお知らせします． -------------------------------------------------------------------------- 第14回プログラミングおよびプログラミング言語ワークショップ（PPL2012） http://ppl2012.cs.uec.ac.jp/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2012年3月8日(木)〜3月10日(土) 会場: 和歌山県西牟婁郡白浜温泉むさし http://www.yado-musashi.co.jp/ PPL2012は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ１: 国内外で未発表の論文の発表カテゴリ２: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ３: ポスター・デモ発表（既発表・未発表の別を問いません） ※ショートプレゼンテーションは行いませんカテゴリ１の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また，ポスター・デモを含む全発表のなかから，聴衆の投票により，最も優秀なプレゼンテーションに発表賞（一般の部，学生の部）を授与する予定です．カテゴリ１（国内外未発表論文） ------------------------------ 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です（ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません）．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとする予定です．採録された論文は，PPL2012参加者に配布される予稿集に掲載され，参加者のみがアクセス可能な形でWEB上で公開されます（論文へのリンク集ページを作成し，閲覧に必要なパスワードを参加者に連絡します）．カテゴリ１で発表された研究のうち，PPL2012プログラム委員会として優れていると認めるものは，PPL2012終了後（2012年4月下旬予定），「コンピュータソフトウェア」誌PPL2012推薦論文としての投稿が可能です．推薦論文は，PPLプログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ２（国外既発表論文） ---------------------------- 査読付の国際会議または学術雑誌等で既発表であるが，国内では未発表な研究の紹介をする場です．採録決定済みの研究も含みます．PPLへの関連をもとに採録を判定いたします．カテゴリ３（ポスター・デモ発表） -------------------------------- ２時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また，申込多数の場合は抽選によって採否を決定する可能性があります．なお，PPL2012ではポスターやデモによる活発な意見交換を促進したいという観点から，ショートプレゼンテーションのセッションは設けません．招待講演 -------- 長谷川真人（京都大学）細谷晴夫（理化学研究所脳科学総合研究センター・科学技術振興機構さきがけ）以上のお二方の招待講演を予定しています． ====================================================================== 投稿・発表申込要領３つのカテゴリそれぞれに対して，投稿は以下のように行って下さい．最新の情報は上記Webページでご確認下さい．カテゴリ１（国内外未発表論文） ------------------------------ 投稿手続きは二段階です．発表申込を行った上で論文提出を行って下さい． (注) 採録された論文等著作物は，日本ソフトウェア科学会著作権規定 (http://www.jssst.or.jp/files/user/edit/chosakuken-kitei.pdf) にもとづいて利用されますので，予めご確認ください． (注) カテゴリ１への投稿論文と類似の論文を，他の会議（予稿集を出版するもの）・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記して下さい．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります（他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります）．発表申込先：https://www.easychair.org/conferences/?conf=ppl2012 発表申込締切：2011年12月22日(木) 著者名，所属，論文タイトル，論文概要（日本語300〜400字程度もしくは英語200 words程度）を提出してください．上記webページのフォームに入力する日本語の文字コードはすべてUTF-8にしてください． (注) フォームにおいて，change informationをクリックすると文字化けが発生する場合がありますが，情報の登録は正しく行なわれますので問題ありません．論文提出締切：2012年1月6日(金) 10ページ程度（最大15ページ）の論文（英語もしくは日本語，PostScriptもしくはPDF形式）を提出して下さい．採否通知：2012年1月31日(火) 最終原稿提出締切：2012年2月13日(月) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします．カテゴリ２（国外既発表論文） ---------------------------- 昨年同様，カテゴリ2の申込締切が少し早くなっていますのでご注意ください．締切直後（2月初旬頃）に採否が決定する国際会議については，あらかじめ，下記問い合わせ先までご相談ください． (注) 申込時はabstractをテキスト形式でお送りください．最終原稿は，下記のスタイルファイルを利用したpdfにてお送りください．発表申込先：ppl2012-submit(a)kuis.kyoto-u.ac.jp 発表申込締切：2012年1月23日(月) 原論文（ページ数不問，PostScriptもしくはPDF形式）とabstract（テキスト形式）を，著者名，所属，論文タイトル，原論文の出典（発表会議名，掲載済／予定の別等）と併せて上記申込先宛にお送り下さい．採否通知：2012年1月31日(火) 最終原稿提出締切：2012年2月13日(月) カテゴリ３（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行なわずに募集いたします．デモを行なう場合は，発表概要においてその旨をご説明ください．発表申込先：ppl2012-submit(a)kuis.kyoto-u.ac.jp 発表申込締切：2012年2月6日(月) 著者名，所属，発表タイトル，発表概要（200〜300字程度），希望する発表形態（ポスター・デモの別），をテキスト形式で上記申込先宛にお送り下さい．採否通知：2012年2月13日(月) ワークショップ全般に関する問い合わせ先：ppl2012-oc(a)kuis.kyoto-u.ac.jp ====================================================================== プログラム委員会青戸等人 (東北大学) 稲葉一浩 (Google) 上野雄大 (東北大学) 小笠原啓 (ITプランニング) 角谷良彦 (東京大学) Jacques Garrigue (名古屋大学) 小宮常康 (電気通信大学) 立堀道昭 (IBM東京基礎研究所) 千代英一郎 (日立製作所) 中澤巧爾 (京都大学) 中田秀基 (産業技術総合研究所) 西村進 (京都大学) 長谷部浩二 (筑波大学) 浜名誠 (群馬大学) 前田敦司 (筑波大学) 八杉昌宏 (京都大学) 横山大作 (東京大学) 渡部卓雄 (東京工業大学) 実行委員会鵜川始陽 (電気通信大学) [実行委員長] 中澤巧爾 (京都大学) [プログラム共同委員長] 前田敦司 (筑波大学) [プログラム共同委員長] --------------------------------------------------------------------------

1 0

Kobe Kolloquiun on Logic, Statistics and Informatics
by fuchino＠isc.chubu.ac.jp 04 Dec '11

04 Dec '11

We announce the following talk in Kobe Colloquium on Logic, Statistics and Informatics: ------------------------------------------------------------------------- Date and time: Dec. 12, 2011 (Mon.), 15:10 -- 16:40 Place: Presentation Room of "Fuchino Group" on the 4th Floor of Science and Technology Research Building 3 (Shizenkagakutou Sangokan) (see: http://www.kobe-u.ac.jp/en/access/rokko/campus.htm) Speaker: Professor Dr. Peter Vojtas (Department of Software Engineering of the Charles University in Prague) Title of the talk: Soundness and completeness of fuzzy Prolog/Datalog. ------------------------------------------------------------------------- Abstract: We start with using user preference search as a motivation for a many valued (fuzzy) model of Prolog/Datalog/Querying. We mention problems of classical approach with refutation and clausal rules. We base our semantics on implicative rules and many valued modus ponens. We prove soundness and completeness of our semantics. We discuss also clausal approach and fuzzy resolution. -- best regards Saka\'e Fuchino (渕野昌) ------------------------------------------------------------------------- Kobe University Graduate School of System Informatics Rokko-dai 1-1, Nada, Kobe 657-8501 e-mail: fuchino(a)diamond.kobe-u.ac.jp web page: http://kurt.scitec.kobe-u.ac.jp/~fuchino/ -------------------------------------------------------------------------

1 0

LATD2012
by Hiroakira Ono 01 Dec '11

01 Dec '11

Logic, Algebra and Truth Degrees 2012 http://www.jaist.ac.jp/rcis/latd12/ First Call for Papers The third official meeting of the EUSFLAT Working Group on Mathematical Fuzzy Logic [1] will be held on 10-14 September 2012 in Kanazawa, Japan. The conference is organized by Research Center for Integrated Science [2], Japan Advanced Institute of Science and Technology [3]. Mathematical Fuzzy Logic is a subdiscipline of Mathematical Logic which studies the notion of comparative truth. The assumption that 'truth comes in degrees' has proved to be very useful in many, both theoretical and applied, areas of Mathematics, Computer Science and Philosophy. The main goal of this meeting is to foster collaboration between researchers in the area of Mathematical Fuzzy Logic, and to promote communication and cooperation with members of neighbouring fields. The featured topics included, but are not limited to, the following: . Proof systems for fuzzy logics: Hilbert, Gentzen, natural deduction, tableaux, resolution, computational complexity, etc. . Algebraic semantics: residuated lattices, MTL-algebras, BL-algebras, MV-algebras, Abstract Algebraic Logic, functional representation, etc. . Game-theory: Giles games, Renyi-Ulam games, evaluation games, etc. . First-order fuzzy logics: axiomatizations, arithmetical hierarchy, model theory, etc. . Higher-order fuzzy logical systems: type theories, Fuzzy Class Theory, and formal fuzzy mathematics. . Philosophical issues: connections with vagueness and uncertainty. . Applied fuzzy logical calculi: foundations of logical programming, logic-based reasoning about similarity, description logics, etc. We also welcome contributions on any relevant aspects of related logical systems (such as substructural and quantum logics, and many-valued logics in general). Conference Web Site: http://www.jaist.ac.jp/rcis/latd12/ Important dates: . 22 April 2012: deadline for submissions . 3 June 2012: notifications sent . 10-14 September 2012: conference Programme Committee: . Stefano Aguzzoli (University of Milano, Italy) . Matthias Baaz (Vienna University of Technology, Austria) . Petr Cintula (Academy of Sciences, Czech Republic) . Carles Noguera (CSIS, Spain) . Hiroakira Ono (JAIST, Japan), Chair . James Raftery (University of KwaZulu-Natal, South Africa) . Constantine Tsinakis (Vanderbilt University, USA) Invited Speakers: . Rostislav Horcik (Academy of Sciences, Czech Republic) . Emil Jerabek (Academy of Sciences, Czech Republic) . Daniele Mundici (University of Florence, Italy) . Greg Restall (University of Melbourne, Australia) . Luca Spada (University of Salerno, Italy) Tutorial: . Felix Bou (CICS, Spain) If you are interested in presenting a paper, please submit a 2‚Äì4 pages abstract at http://www.easychair.org/conferences/?conf=latd2012 Your submission will be confirmed automatically on the e-mail address you provide. The accepted abstracts will be available on-line after the final decision of the program committee. If you have any problems to submit an abstract, please contact us at mail to: latd2012(a)jaist.ac.jp The deadline for contributions is 22 April 2012. The notification of acceptance/rejection will be sent until 3 June 2012. Conference dates: The scientific program will start Monday morning (10 September) and finish Friday noon (14 September). Wednesday afternoon we plan an excursion. Venue: The conference will be held in the city of Kanazawa [4,5,6], located in the Ishikawa prefecture of Japan on the Japan Sea. The venue is the Ishikawa Prefectural Museum of Art [7] in the center of Kanazawa. Local Organizing Committee: . Norbert Preining (JAIST, Japan), Chair . Katsuhiko Sano (JAIST, Japan) . Kazushige Terui (Kyoto University, Japan) . Shunsuke Yatabe (AIST, Japan) For further information please contact: latd2012(a)jaist.ac.jp [1] http://www.mathfuzzlog.org/ [2] http://www.jaist.ac.jp/rcis/en/ [3] http://www.jaist.ac.jp/ [4] http://en.wikipedia.org/wiki/Kanazawa,_Ishikawa [5] http://www.kanazawa-tourism.com/ [6] http://wikitravel.org/en/Kanazawa [7] http://www.ishibi.pref.ishikawa.jp/index_j.html

1 0

Kobe Colloquium on Logic, Statistics and Informatics: 1 Dec., 2011
by Hirotaka Kikyo 25 Nov '11

25 Nov '11

皆様桔梗宏孝＠神戸大学システム情報学研究科です． 2011年12月1日（木）の 17：00 から下記のように Lyon 1 大学の Amador Martin-Pizarro 氏によるモデル理論におけるMorleyの定理に関する神戸情報数理コロキウムの講演を予定しております．講演者の Amador Martin-Pizarro 氏には，モデル理論の専門の方だけでなくロジック全般の general audience 向けの講演になるよう，お願いしてあります．興味のある方は御参加ください．なお，この回の次の神戸コロキウムでは，2011年12月12日 15：10 から Professor Peter Vojtas (Charles Univ. (プラハ大学)) による many valued Prolog に関する講演を予定しております．これについては改めてご案内いたします． ---------------------------------------------------------------------------------- 神戸情報数理コロキウム日時：2011年12月1日（木）17:00 〜 18:30 場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループ内プレゼンテーション室）講演者： Amador Martin-Pizarro (リヨン１大学) 題目： Morley's theorem and Geometric Model Theory アブストラクト：A countable theory is uncountably categorical if it only has a unique model (up to isomorphism) on each uncountable cardinal. Morley proved that a theory is uncountably categorical if it is categorical on cardinality the continuum. His proof uses the fact that every model can be built from basic bricks, called strongly minimal sets (which generalise the concept of an absolutely irreducible algebraic curve). The goal of this talk is to give an overview (to a general audience) of some of the ideas of the proof based on examples. Moreover, we will link the classification of strongly minimal sets to results in other areas of mathematics, specially number theory, such as the existence of infinite Mersenne primes and Schanuel's conjecture. ------------------------------------------- 神戸大学自然科学総合研究棟3号館への行き方： http://kurt.scitec.kobe-u.ac.jp/~kikyo/seminar/scitec3.pdf

1 0

セミナー案内
by KASHIMA Ryo 24 Nov '11

24 Nov '11

数理論理学セミナーのご案内日時：10月27日(木)17時から場所：東京工業大学大岡山キャンパス西８号館Ｗ棟 10階 W1008セミナー室話者：堀畑佳宏（東北大）題目：弱い算術とconcatenationの理論概要：文字列の結合に関する理論（concatenationの理論） TC は、2005年に Grzegorczyk によって導入され、その決定不可能性が示された。一方、2009年にはVisser, Svejdar, Ganea がそれぞれ独立に、TC が Robinson 算術 Q と互いに翻訳可能であることを示した。本発表では、concatenation の理論 WTC を新たに導入し、この理論が Robinson と Tarski によって導入された非常に弱い算術 R と互いに翻訳可能となることを見る。 ---------- 会場までの交通案内はこちらから： http://www.titech.ac.jp/about/campus/index.html ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp ＃＃＃木曜夕方を中心に不定期的にセミナーを開催しています。＃＃＃＃＃＃詳細はお問い合わせください。＃＃＃

1 1

Call for Participation: PEPM 2012
by Kohei SUENAGA 24 Nov '11

24 Nov '11

（重複して受け取られた場合はどうぞご容赦ください。）京都大学の末永と申します。来年1月に POPL 2012 と併設で開催される PEPM 2012 のご案内をお送りいたします。今回も日本からの４本の論文を含む見所満載のプログラムになっております。 Early registration は12月24日までとなっております。 POPL ともども皆様の参加をお待ち申し上げております。京都大学末永幸平 ksuenaga(a)sato.kuis.kyoto-u.ac.jp -- ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation http://www.program-transformation.org/PEPM12 January 23-24, 2012. Philadelphia, PA, USA (co-located with POPL'12) Call For Participation Online registration is open at https://regmaster3.com/2012conf/POPL12/register.php Early registration deadline is December 24, 2011 The PEPM Symposium/Workshop series brings together researchers and practitioners working in the broad area of program transformation, which spans from refactoring, partial evaluation, supercompilation, fusion and other metaprogramming to model-driven development, program analyses including termination, inductive programming, program generation and applications of machine learning and probabilistic search. PEPM focuses on techniques, supporting theory, tools, and applications of the analysis and manipulation of programs. In addition to the presentations of regular research papers, the PEPM program includes tool demonstrations and `short paper' presentations of exciting if not fully polished research. PEPM has established a Best Paper award. The winner will be announced at the workshop. INVITED TALKS Compiling Math to High Performance Code Markus Pueschel (ETH Zuerich, Switzerland) http://www.inf.ethz.ch/~markusp/index.html Specification and verification of meta-programs Martin Berger (University of Sussex, UK) http://www.informatics.sussex.ac.uk/users/mfb21/ ACCEPTED PAPERS Regular research papers: Naoki Kobayashi, Kazutaka Matsuda and Ayumi Shinohara. Functional Programs as Compressed Data Kazutaka Matsuda, Kazuhiro Inaba and Keisuke Nakano. Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals Dana N. Xu. Hybrid Contract Checking via Symbolic Simplification Susumu Katayama. An Analytical Inductive Functional Programming System that Avoids Unintended Programs Roberto Giacobazzi, Neil Jones and Isabella Mastroeni. Obfuscation by Partial Evaluation of Distorted Interpreters Michael Gorbovitski, Yanhong A. Liu, Scott Stoller and Tom Rothamel. Composing Transformations for Instrumentation and Optimization Elvira Albert, Jesus Correas Fernandez, German Puebla and Guillermo Roman-Diez. Incremental Resource Usage Analysis Takumi Goto and Isao Sasano. An approach to completing variable names for implicitly typed functional languages Martin Hirzel and Bugra Gedik. Streams that Compose using Macros that Oblige Vlad Ureche, Tiark Rompf, Arvind Sujeeth, Hassan Chafi and Martin Odersky. StagedSAC: A Case Study in Performance-Oriented DSL Development Markus Degen, Peter Thiemann and Stefan Wehr. The Interaction of Contracts and Laziness Surinder Kumar Jain, Chenyi Zhang and Bernhard Scholz. Translating Flowcharts to Non-Deterministic Languages Francisco Javier Lopez-Fraguas, Enrique Martin-Martin and Juan Rodriguez-Hortala. Well-typed Narrowing with Extra Variables in Functional-Logic Programming Geoff Hamilton and Neil Jones. Superlinear Speedup by Distillation: A Semantic Basis Short papers: Jacques Carette and Aaron Stump. Towards Typing for Small-Step Direct Reflection Janis Voigtlaender. Ideas for Connecting Inductive Program Synthesis and Bidirectionalization Tool demonstration papers: Edvard K. Karlsen, Einar W. Hoest and Bjarte M. Oestvold. Finding and fixing Java naming bugs with the Lancelot Eclipse plugin Adriaan Moors, Tiark Rompf, Philipp Haller and Martin Odersky. Scala-Virtualized Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gomez-Zamalloa and German Puebla. COSTABS: A Cost and Termination Analyzer for ABS

1 0

Workshop on Juris-informatics (JURISIN 2011)の開催のお知らせ
by Ken Satoh 16 Nov '11

16 Nov '11

各位今年の12/1-2に高松でJSAI-IsAIの一部として開催される法律と情報学のワークショップJURISIN2011 http://research.nii.ac.jp/~ksatoh/jurisin2011.html のプログラムをお送り致します。多数の方のご参加をお待ちしております。登録は、 http://www.ai-gakkai.or.jp/jsai-isai/2011/#registration の情報をご覧ください。 12/1には法言語学(Forensic Linguistics)研究で有名な明治大学法学部の堀田秀吾教授 12/2にはIJCAIでResearch Excellence Awardを受賞したKowaski教授の招待講演があります。どうぞよろしくお願いいたします。佐藤　健国立情報学研究所 =============================================================== JURISIN 2011 Program Dec. 1, 2011 12:45-13:00 Opening Remark: Ken Satoh (National Institute of Informatics and Sokendai) 13:00-14:00 Invited Talk I Implications of Forensic Linguistics for Juris-informatics Syugo Hotta (Meiji University) 14:00-14:30 Document Structure Analysis with Syntactic Model and Parsers: Application to Legal Judgments Hirokazu Igari, Akira Shimazu and Koichiro Ochimizu 14:30-15:00 Recall-Oriented Evaluation Metrics for Consistent Translation of Japanese Legal Sentences Yasuhiro Ogawa, Masaki Mori and Katsuhiko Toyama 15:00-15:30 Using Classification to Support Legal Knowledge Engineers in the Eunomos Legal Document Management System Luigi Di Caro, Llio Humphreys and Guido Boella 15:30-16:00 Coffee Break 16:00-16:30 Prerequisite-Effect Structure on Intuitionistic Kripke Model Katsuhiko Sano, Shingo Hagiwara and Satoshi Tojo 16:30-17:00 The Concept and Definition of Software Accountability in Legal Engineering Ryo Hayasaka and Koichiro Ochimizu Dec. 2, 2011 9:30-10:30 Invited Talk II WUENIC: A Case Study in Rule-based Knowledge Representation and Reasoning Robert Kowalski(Imperial College London) and Anthony Burton 10:30-11:00 Coffee Break 11:00-11:30 A Substance-Field based Argumentation Framework Wachara Fungwacharakorn, Nuanwan Soonthornphisaj and Boonserm Kijsirikul 11:30-12:00 Deliberation Process Support System for Citizen Judge Trial Based on Structure of Factors Takanori Sato, Shogo Okada and Katsumi Nitta 12:00-12:30 A Semantics of Argumentation under Incomplete Information Ken Satoh and Kazuko Takahashi 12:30-12:45 Concluding Remark: Ken Satoh (National Institute of Informatics and Sokendai)

1 0

Call for Participation: LENLS 8 (Logic and Engineering of Natural Language Semantics 8)
by BEKKI Daisuke 15 Nov '11

15 Nov '11

（重複して受け取られた場合はご容赦ください）今年の12/1-3に高松で開催される LENLS8 国際ワークショップのプログラムをお送り致します。多数の方のご参加をお待ちしております。 12/3にはアムステルダム大学のFrank Veltman先生、青山学院大学のEric McCready先生によるチュートリアル講演を予定しています。戸次大介（お茶の水女子大学）照会先：lenls8 [[at]] easychair.org [Apologies for multiple copies] ================================================================= CALL FOR PARTICIPATION Logic and Engineering of Natural Language Semantics 8 (LENLS8) Workshop Site : "Sunport Hall Takamatsu", Takamatsu 2-1, Sunport, Takamatsu-shi, Kagawa-ken, Japan Information/Registration： 5th Floor Conference Rooms： 5th and 6th Floor Dates : December 1-3, 2011 Contact Person: Alastair Butler Contact Email : lenls8(a)easychair.org Website : http://www.is.ocha.ac.jp/‾bekki/lenls/ ================================================================= Chair: Alastair Butler (JST/Tohoku University) Invited Speaker(s): Frank Veltman (University of Amsterdam) Kentaro Inui (Tohoku University) Information on Takamatsu: http://www.takamatsu.or.jp/eng/ http://www.city.takamatsu.kagawa.jp/english/access/ http://www.my-kagawa.jp/eg/ LENLS is an annual international workshop focusing on formal semantics and pragmatics. It will be held as one of the workshops of JSAI isAI 2011, sponsored by The Japan Society for Artificial Intelligence (JSAI). Registration ============ The proceedings of the workshop will be available at the conference site for registered persons. Please follow the link below and register yourself until 24th November 2011. http://www.ai-gakkai.or.jp/jsai-isai/2011/index.html#registration Program ======= December 1st (Thu), 2011 ------------------------- 09:00-10:00: Reception 10:00-10:10: Opening Remarks 10:10-11:40: Session 1 * Yoshiki Mori "Back To the Future, Back From the Future - To and Fro For the Counterfactual Future In the Past -" * Yurie Hara, Yuli Feng and Shigeto Kawahara "Emphatic Stress as Epistemic Conflict: A case study of Mandarin Chinese" * Chungmin Lee "Dynamic Perspective Shifts in Evidentials: Evidence from Korean" 11:40-13:00: Lunch 13:00-15:00: Session 2 * Mauricio Hernandes "Players who don't know how to play. An Haskell implementation of unawareness." * Oleg Prosorov "A Sheaf-Theoretic Framework for Dynamic Semantics" * Margot Colinet and Gre'goire Winterstein "Linking probabilistic accounts: polarity items and discourse markers" * Hiroko Ozaki and Daisuke Bekki "Extractability as Deduction Theorem in Subdirectional Combinatory Logic" 15:00-15:30: Coffee break 15:30-16:30: Session 3 * Gre'goire Winterstein "Ludics and Presupposition Projection" * Nicholas Asher and Jason Quinley "Begging Questions, Getting Answers and Basic Cooperativity" 16:30-17:30: Invited Talk 1 * Frank Veltman (University of Amsterdam) "(TBA)" December 2nd (Fri), 2011 ------------------------- 08:30-09:00: Reception 09:00-10:30: Session 4 * Yo Sato and Wai Lok Tam "Underspecified types and the semantic bootstrapping of common nouns and adjectives: a simulation with a robot's sensory data " * David Yoshikazu Oshima "The Japanese particle yo in declaratives: Relevance, priority, and blaming" * Katsuhiko Yabushita "Japanese NPI Dare-mo as Unrestricted Universal Quantifier" 10:30-11:00: Coffee break 11:00-12:00: Session 5 * J.-R. Hayashishita and Daisuke Bekki "Conjoined nominal expressions in Japanese: Interpretation through monad" * Christina Unger "Dynamic semantics as monadic computation" 12:00-13:30: Lunch 13:30-15:00: Session 6 * Satoru Suzuki "Measurement-Theoretic Foundations of Gradable-Predicate Logic" * Tzu-Keng Fu "Universal Logic and the Logical Many-valuedness" * Alastar Butler and Kei Yoshimoto "Towards a self-selective and self-healing evaluation" 15:00-15:30: Coffee break 15:30-16:30: Invited Talk 2 * Kentaro Inui (Tohoku University) "Toward Deep Processing of Language in the Era of Large-scale Knowledge Resources: Time for Formal Semantics to Meet NLP Again" Alternates ---------- * Eric Mccready "Trust in Evidential Testimony" December 3rd (Sat), 2011 ------------------------- On the 3rd December, there will also be special tutorial lectures at the workshop venue by Frank Veltman (University of Amsterdam) and Eric McCready (Aoyama Gakuin University). Lecturer: - Frank Veltman (University of Amsterdam) - Eric McCready (Aoyama Gakuin University) Location: "Sunport Hall Takamatsu", Takamatsu 2-1, Sunport, Takamatsu-shi, Kagawa-ken, Japan Time Table (Tentative): 10:00-12:00 Session 1: Tutorial Lecture by Eric McCready Title: (TBA) 12:00-13:30 Lunch 13:30-17:30 Session 2: Tutorial Lecture by Frank Veltman Title: "Or else, what?" Abstract: In this talk I will present the theory of imperatives that I have developed in the past five years and apply it to a number of problems involving disjunction. In particular I will use it to analyse pseudo-imperatives and a variant of the Miners Paradox. Organizing Committee ==================== Alastair Butler (Chair) Daisuke Bekki Eric McCready Yoshiki Mori Yasuo Nakayama Katsuhiko Yabushita Tomoyuki Yamada Shunsuke Yatabe Kei Yoshimoto Contact ======= lenls8 [[at]] easychair.org

1 0

Call for papers Special issue of Logic Journal of IGPL *** Non-classical Modal and Predicate Logics ***
by Yuping Shen 15 Nov '11

15 Nov '11

(Apologies for multiple copies) Call for papers *** Non-classical Modal and Predicate Logics *** special issue of Logic Journal of IGPL Modalities and predicates have since ancient time been central notions in logic. In the 20th century, various systems of non-classical logics have emerged, with applications in many disciplines like Computer Science, Linguistics, Mathematics, and Philosophy. This gave rise to the questions of non-classical treatment of quantification and modalities and their accommodation in these non-classical settings. In response, various modal and predicate variants of non-classical logics have been introduced and studied in the past decades. This special issue is solely dedicated to modal and predicate non-classical logics. Its aim is to bring together papers from various branches of non-classical logics, not only to present recent advances in the particular fields, but also to identify common problems and methods and foster the exchange of ideas between researchers from separate fields. Topics of interest: * The study of first- or higher-order variants of non-classical logics, including, but not limited to: - Predicate intuitionistic and superintuitionistic logics - Predicate modal logics - Predicate substructural logics - Predicate many-valued and partial logics - Predicate paraconsistent logics - Predicate non-monotonic logics, etc. * Non-classical theories of quantification over classical logic, such as: - Free logics - Branching quantifiers and IF-logic - Generalized quantifiers * Extensions by modalities of (propositional or predicate) non-classical logics, including: - Modal extensions of (super)intuitionistic, substructural, many-valued, paraconsistent, non-monotonic, etc., logics - Co-algebraic treatment of modalities We encourage to submit papers on the above logics from any branches of mathematical logic (proof-theory, model theory, game theory, complexity, etc.), be it purely theoretical or about applications in the foundation of mathematics, computer science, linguistics, and philosophy. == Deadline == 31 March 2012 == Submissions == Papers should be submitted to ncmpl(a)cs.cas.cz. Please also use this email to express interest in submitting a paper. == A related conference == This special issue is related with the conference Non-classical Modal and Predicate Logics, organized Guangzhou (Canton), China, 5-9 December, 2011. http://logic.sysu.edu.cn/ncmpl2011 Petr Cintula, Rosalie Iemhoff, Shier Ju guest editors

1 0

「論理学と数学の哲学に関する研究会」のお知らせ
by Shunsuke Yatabe 08 Nov '11

08 Nov '11

「論理学と数学の哲学に関する研究会」のお知らせ日本科学哲学会第44回大会のサテライトイベントとして、以下の研究会を開催いたします。奮ってご参加ください。本研究会は、論理学および数学の哲学に関するテクニカルな研究に関する情報交換を行うための研究会です。通常の学会では発表は20分程度であり、テクニカルなテーマについて詳細な突っ込んだ議論を行うことが出来ません。そこで、本研究会では、テクニカルなテーマについての発表を、質疑応答も含め一人あたり一時間半程度おこない、議論を深めよう、ということを目的としています。 * 日時：2011年11/21（月）9:00-18:30 * 会場：星陵会館（永田町・赤坂見附） 1階会議室Ｆ http://www.seiryokai.org/kaikan.html * タイムテーブル： o 午前の部：グレアム・プリースト「存在しないものに向かって」　　　　　　　　　　　翻訳本刊行記念セッション + 9:00-10:30 久木田水生（京都大学）：　　　　　　　　　　　　記述句の多義性 + 10:45-12:15 藤川直也（首都大学東京）：　　　　　　　　　　　『存在しないものに向かって』における内包的他動詞の　　　　　　　　　　　　扱いについて o 午後の部：曖昧性セッション + 13:30-15:00 伊勢田哲治（京都大学）：　　　　　　　　　　　　曖昧述語に関する統計的モデルと主観的確率 + 15:15-16:45 岡本賢吾（首都大学東京）：　　　　　　　　　　　　遷移・文脈的変項・無視可能性 ― 動的ハイブリッド　　　　　　　　　　　　論理から曖昧性を考える + 17:00-18:30 矢田部俊介（産業技術総合研究所）：　　　　　　　　　　　　あいまい性と極限ー構成的素朴集合論における余帰　　　　　　　　　　　　納的対象の定義可能性 * Web site: http://researchmap.jp/joeluyy5c-21098/#_21098 * お問い合わせはこちらまでお願いします（[at]を@にお書き換え下さい） o 矢田部俊介( shunsuke.yatabe[at]aist.go.jp ) o 大西琢朗( takuro.onishi[at]gmail.com ) ********************************************************************************** * 講演要旨*** + 久木田水生（京都大学） # 題目：記述句の多義性 # 要旨：記述句を含む文（以下「記述文」）の評価（意味の決定）には根本的に異なる二つの方法がある。一つは「マイノング的評価」であり、そこでは記述句は名前と同様に対象を指示する項として扱われる。しかしながら記述句の中には「現在のフランス国王」のように、指示対象が存在しないものもあるため、マイノング的評価においては、記述句（あるいは一般に項）によって存在しない対象を指示することが可能でなければならない。もう一つは「ラッセル的評価」であり、そこでは記述句は独立した文法的単位とは見なされず、それ自体では指示対象を持たない。従ってここでは「現在のフランス国王」のような記述句が何か存在しない対象を指示するものと見なされる必要はない。このためにマイノング的評価とラッセル的評価の間には、存在しない対象を真正の対象として認めるか否かという、意味論の根本的な枠組みにおける対立が生じる。この二つのどちらが正しい記述文の評価法であるかを決定することは難しい。記述文のある使用例はマイノングを支持するように思われるし、別の使用例はラッセルを支持するように思われる。私たちは場面に応じて異なる評価法を使い分けている、というのが実情であろう。Towards Non-Being(2005)（邦訳『存在しないものに向かって』）においてグレアム・プリーストはマイノング主義に基づいた意味論を提示しており、その意味論では記述文の評価も当然マイノング的である。しかしその一方、プリーストは記述句が異なる場面で異なる使われ方をしていることを認めている。それは記述句が現実に存在する対象を指示するよう意図されている場面と、そうでない場面である。彼は世界意味論の枠組みに依拠しつつ、話者の意図に応じて記述文を評価する舞台となる世界の選び方が変化する、と説明する。しかし彼の説明は、典型的なラッセル的事例（例えば「水星の軌道の内側の惑星が水星の近日点の歳差を引き起こしている」等の文）を分析する際には、不自然であると言わざるを得ない。本発表で私たちはプリーストの意味論がどのように異なる意図で使用されている記述文を取り扱っているかを検討し、マイノング的にせよラッセル的にせよ、一つの評価方法ですべての事例を取り扱うことが困難であるということを指摘する。その上で私たちは二つの異なる評価方法の基盤となるような一般的な意味論的枠組みを提示することを試みる。その意味論は記述句に対して一つの表示を割り当てるという点ではマイノング主義的だが、存在しないものを真正な対象と見なさないという点では反マイノング主義的である。 + 藤川直也（首都大学東京） # 題目：『存在しないものに向かって』における内包的他動詞の扱いについて # 要旨：`seek'や`worship'などに代表されるいわゆる内包的他動詞は、一般に、次の三つ（のうちの少なくとも一つ）の特徴をもつとされる。 * (1) 目的語の名詞句が存在的コミットメントを欠く、 * (2) 目的語において置換可能性が成り立たない、 * (3) 確定的読みと不確定的読み（あるいはrelationalな読みとnotional な読み）をもつ。『存在しないものに向かって』において、プリーストは、非存在主義という一種のマイノング主義に基づいて、内包的他動詞に意味論を与えている。その基本的なアイデアは、例えば`John seeks a unicorn'をおおよそ`∃x(unicorn'(x) & seek'(John, x))'のように分析した上で、量化子を存在中立的なものと見なす（その量化のドメインには、存在する対象のみならず、非存在対象が含まれる）というものだ。この提案は、内包的他動詞の(1)の特徴を直裁的に説明する。さらにプリーストは、内包的他動詞の残る二つの特徴のそれぞれに対して、(1)に対する説明とは独立の説明を与えている。特徴(2)については、彼は、現象そのものを否定する。すなわち、内包的他動詞の目的語に関して、同一指示表現の置換は常に可能であると主張する。また特徴(3)については、不確定的な読みをもつ事例はすべて、なんらかの補文をとる文にパラフレーズ可能であり、不確定的読みはそのようなパラフレーズによって説明されると主張する。　本発表では、プリーストが内包的他動詞に与える意味論と、内包的他動詞の三つの特徴に対する彼の分析を紹介した上で、特に、(i) プリーストは、内包的他動詞の三つの特徴にそれぞれ独立した説明を与えているが、それらは整合的だろうか、(ii) 彼の意味論は、内包的他動詞を含む文に関して妥当に思われる推論、とりわけ目的語の量化名詞句が重要な役割を果たしていると思われる事例を適切に説明できるだろうか、という点に注目しながら、プリーストの提案を検討する。 + 伊勢田哲治（京都大学） # 題目：曖昧述語に関する統計的モデルと主観的確率 # 要旨：発表要旨　 http://researchmap.jp/mug0ywbe4-21099/?action=multidatabase_action_main_fil… 　（pdfファイル）曖昧述語に関しては単純なものから複雑なものまでさまざまなモデルが存在する。しかし、モデルが精緻になればなるほど、「果たしてこれが本当に日常的に使われている曖昧述語の背後に存在する構造なのだろうか」という疑問がわいてこずにはおかない。本発表でめざすのは、確率や統計の比較的単純なモデルのみで曖昧述語を取り扱うことである。一方で、対象自体の性質として、曖昧な対象が存在するように見える。たとえば「赤」から「黄色」への色のグラデーションにおいて赤と黄色の「唯一の本当の境目」があるというのは非常にありそうにない。他方で、われわれは曖昧な対象に対して二値的な用法を受け入れているように見える。たとえば、「このリンゴは赤い」といった表現は「はい」か「いいえ」で答えられる問いであるように見える。曖昧述語はなんらかの意味で確率と関わるように見えるけれども、上記のような特徴を考えるなら、単純なベイズ主義で曖昧述語を取り扱うのは難しそうに思われる。そこで導入するのが、重付置主義をベースとした統計モデルである。本発表で提示する統計モデルの概要をまず紹介する（このモデルは2011年7月に第14回CLMPSにおいて発表したものである）。曖昧述語の解釈に使われる基本的なモデルは、重付置主義で言うところの「精密化」(precisification)が一定の統計的分布をとるというモデルである。与えられた状況下で、曖昧述語Fの外延と反外延の間の精密な線を引くという決定（精密化決定）を繰り返し行うものとする。この線の場所としてある値は選ばれやすく、別の値は選ばれにくい、という形で精密化決定は一定の分布φを形成すると考えられる。この手続きは「誤差」のある測定に非常に似ている。そのアナロジーを推し進めるなら、「最小二乗法を使って真の境界線を推定する」といった行き方も考えられる。しかしすでに述べたように、曖昧述語はそもそも真の境界線を持たないような述語だと考えられるので、そうした推定は場違いであると思われる。それにかわって本発表で採用するのは、還元主義的戦略、すなわち、曖昧述語の意味の本体はこの精密化決定の分布φそのものであり、曖昧述語の二値的用法も最終的にはこの確率分布に還元される、という考え方である。二値的な用法の導入の仕方として、「重付置主義的解決」と「ベイズ的解決」を考える。重付置主義的解決とは、分布φを元に「許容可能性」に類する区別を導入するという考え方である。この場合、曖昧述語は重付置主義における重真と同じような簡単な様相論理的性質を持つことができる。もう一つのベイズ主義的解決とは、「次の精密化決定は与えられた対象XをＦの外延の側に入れる」という命題の事後確率を考え、その確率が十分に小さければ「ＸはＦではない」を受け入れる、という考え方である。これはベイズの定理を使うという意味でベイズ的とはいえ、分布は統計的分布であり、また統計的検定における有意水準に似たアイデアを使うなど、単なるベイズ主義とはひと味違うものになっている。以上が曖昧述語の統計的モデルの概要であるが、本発表ではこれにさらに主観的確率の要素を付け加える。統計的モデルの基礎となっている精密化決定の分布φは、仮想的なものであり、われわれが曖昧述語を使う際に事前の情報として持っているとは考えにくい。したがって、実際に曖昧述語を使う際には、さらにこの分布についての主観的な確率に基づいて判断する、という、もう一段階の不確実性が持ち込まれていると考えられる。二段階目の不確実性を導入する方法はいくつか考えられるが、上記のベイズ的解決を採用するなら、「次の精密化決定は与えられた対象XをＦの外延の側に入れる」という命題に対する主観的な事後確率を与える形が考えられる。このような手順で考えるならば、曖昧性が対象自体の性質であり、しかもわれわれはそれらについて二値的に語る、という状況において、主観的確率を使った判断が可能となる。 + 岡本賢吾（首都大学東京） # 題目：遷移・文脈的変項・無視可能性――動的ハイブリッド論理から曖昧性を考える # 要旨：発表要旨 http://researchmap.jp/muf24r5dr-21099/?action=multidatabase_action_main_fil… （pdfファイル）（以下は要旨pdfファイル[1]部からの抜粋）本発表は，2011年7月17日に「哲学若手研究者フォーラム」で話した内容の増補改訂版である。例えば、熱力学などのマクロ物理学のうちには，曖昧述語を用いた推論事例（として再構成しうるもの）が、実はごく当たり前に含まれていると考えられる。その典型は、当日述べる通り、「無視しうる（negligible）大きさ」が登場する様々の論証などである。このような熱力学などの論証については、とりわけ次の事実が注目される。すなわちそこでは、曖昧性をめぐる通常の哲学的議論のうちで「toleranceの原理」と呼ばれているもの――曖昧述語の適用基準には許容性がある，すなわち例えば，身長r cmの人が「背が高い」ならばr−10＾-1 cmの人もそうである、等々―― が、一定の仕方で受け入れられており、この原理への（少なくとも暗黙の）アピールがほぼ不可欠に生じていると解される、ということである。ところが他方で、現在、かなりの数の哲学者――通常のsuper-valuation主義者、真理値degree 論者、fuzzy論理支持者、等々のほぼすべて――は、「toleranceの原理」は妥当ではありえないと主張している。だがそうなると、彼らが正しいとする限り、熱力学の論証においては、不当な原理へのアピールという極めて不可解なこと――そのままでは論理的に許容し難いこと――が起こっていることになってしまう。これは看過できない問題である。もちろん、そうは言っても、「toleranceの原理」を受け入れる路線に転向する以外に一切対処策がないということにはならない。例えば、この原理へのアピールを含まない形へ熱力学の論証を書き換えるといったこともおそらく不可能ではないだろう。しかし、そうした書き換えは決して簡単ではないと予想されるし（少なくとも、一様な仕方ですべての論証を書き換える手続きを与えるのは相当に難しいだろう）、それ以前の問題として、既存の科学で受け入れられている論証に対して、そのような大幅な書き換えを要求するとしたら、それはむしろ、要求する側の考えに何か問題がある（当該の科学の論証を分析し損ねている公算が高い）と見るべきであるように思われる。要するに、 super-valuation、真理値degree論、fuzzy論理、等々を持ち出す分析は、もちろんそれぞれに独創的で、論理技術のエキジビションとしては十分興味深く啓発的なのだが、しかし曖昧述語の現実の用法の解明としては、多分に空想的・思弁的であり、あまり的確に的を射ていない疑いがある、ということである。　これに対して、今回、発表者は次のことを試みる。すなわち，以下の［２］で略述するような論理的枠組みを用いれば――この枠組みは，もともとtoleranceの原理を擁護すること（この原理を、他の原理と矛盾することのない仕方で、受け入れ可能なものとして定式化可能にさせること）をその基本的動機としている――、実際に当該の熱力学的論証の妥当な形式化が可能となる、ということである。これにより、(i)発表者の提案が、上記のような多くの哲学者たちのアプローチとは異なり、曖昧性述語の現実の用法に即した十分なリアリティーを備えたもの（とまで言えるかは判らないが，ともかくそうした望みを持ったもの）であること， (ii)もっと基本的な問題として，曖昧性についての通常の哲学的議論において安易に前提されがちなある種の考え、つまり、「曖昧述語は自然言語の特異的な特性である」とか「もっぱら現象的性質を表すものである」といった考えが，単なる誤った思い込みに過ぎないこと、等々の結論を引き出しうるであろう．本発表の目標は、基本的にこうした点にある。 + 矢田部俊介（産業技術総合研究所） # 題目：あいまい性と極限ー構成的素朴集合論における余帰納的対象の定義可能性とその影響について # 要旨：曖昧さを表現できるような弱い論理体系においては、同時に包括原理などの対象の循環的定義を許す原理を仮定しても無矛盾であることが知られている。本発表では、構成的な部分構造論理の一つである Flew∀ （直観主義論理から縮約規則を除去した体系）上の素朴集合論 CONS を例に取り、包括原理を仮定することは、言語を豊かにするだけでなく、一方で文の極限を取る（一見メタな）余帰納的操作さえ可能にしてしまうことを示す。具体的には、CONS 上の算術においては、後者関数に関する不動点を定義することが可能である。そしてこの不動点は、自然数全体の集合ωに関し排中律が成立する（∀x（ｘ∈ω∨¬x∈ω））ことが CONS では証明できないことを保証する。このキーとなる不動点は、余帰納的に定義された対象であり、後者関数を取るという操作の極限であると見なせる。通常、排中律は対象の確定性を表現すると考えられるため、極限操作が排中律に対する反例を提供するという事実は示唆的である。また、この証明を紹介すると同時に、素朴集合論内部における余帰納的な文・対象の定義可能性について議論する。 -- Shunsuke Yatabe <shunsuke.yatabe(a)aist.go.jp> AIST/CRTV (National Institute of Advanced Industrial Science and Technology/ Collaborate Research Team for Verification) tel: +81-6-6494-8047 fax: +81-6-6494-8073

1 0

「ロボットは東大に入れるか」シンポジウムのご案内
by noriko arai 07 Nov '11

07 Nov '11

みなさま、いつもお世話になります。新井紀子＠情報研です。国立情報学研究所では、以下のようなシンポジウムの開催を予定しております。ふるってご参加いただけますようお願いいたします。新井　紀子 **********************************************以下、乞う転載************* 国立情報学研究所（以下NII）では、12月14日（水）、「人工頭脳プロジェクト」キックオフシンポジウムを開催します。　本プロジェクトは、NIIが中心となって1980年以降細分化された人工知能分野を再統合することで新たな地平を切り拓くことを目的に、若い人たちに夢を与えるプロジェクトとして発足しました。日本における学際的な知識・先端技術を集積し、ひいては国際連携を視野に研究活動をスタートさせるため、この度キックオフシンポジウムを開催します。　本プロジェクトの具体的なベンチマークとして、2016年までに大学入試センター試験で高得点をマークすること、また2021年に東京大学入試を突破することを目標に研究活動を進めています。これまで蓄積された人工知能の各要素技術の精度を高め、情報技術分野の未来価値創成につなげるとともに、人間の思考に関する包括的な理解を内外の研究者とともに深めていきたいと考えております。　シンポジウムでは、松原仁氏（公立はこだて未来大学教授）を迎え基調講演を、また、作家の瀬名秀明氏を司会に迎え「知性と知識のはざまで」と題したパネルディスカッションを行います。　国立情報学研究所「人工頭脳プロジェクト」キックオフシンポジウム「ロボットは東大に入れるか」●日時：平成23年12月14日（水）13時20分〜17時30分●会場：学術総合センター一橋記念講堂　　　　〒110-8712 東京都千代田区一ツ橋２−１−２●URL：「ロボットは東大に入れるか」 http://21robot.org/※上記ウェブサイトで参加申込を受け付けています。※入場無料、定員450名（定員に達し次第申込を締め切らせて頂きま… Research、ジェイシー教育研究所プログラム概要：＜第一部＞　講演会基調講演　（松原仁・公立はこだて未来大学）人工知能のグランドチャレンジ　−チェス、サッカー、クイズから東大入試へ− 「ロボットは東大に入れるか」プロジェクト概要説明（新井紀子・NII）「人工知能にとってなぜ大学入試はチャレンジングか」（稲邑哲也・NII）「知識を問う問題にコンピュータはどれだけ答えられるか」（宮尾祐介・NII）＜第二部＞　パネルディスカッション「知性と知識のはざまで」司会　瀬名秀明（作家）安西祐一郎（日本学術振興会）、喜連川優（東京大学）、松原仁、新井紀子 -- --------------------------------------------- Noriko Arai National Institute of Informatics http://researchmap.jp/arai_noriko/

1 0

NIIレクチャーシリーズのお知らせ(Thomas Agotnes)
by Ken Satoh 06 Nov '11

06 Nov '11

NIIレクチャーシリーズのお知らせ国立情報学研究所(NII)では、海外の情報学に関係する著名研究者を招聘し、レクチャーシリーズを行っております。今回は、論理学によるマルチエージェントシステム、ゲーム理論の定式化を研究されているノルウェーのベルゲン大学のThomas Agostnes先生の連続レクチャーのお知らせです。講師:Professor Thomas Agotnes from University of Bergen, Norway. 講義名：Social Laws for Multi-Agent Systems: Logic and Games 　　　　　詳しい講演の内容は、 http://www.nii.ac.jp/en/calendar/2011/121302/ 　をご覧ください。場所：国立情報学研究所 20階 2001 または2010室講義日：2011年 12/13, 20, 27, 2012年1/10, 17, 24, 31 時間: 15:30-17:00 出席は無料で、どなたでも参加できます。なお、CTL(computational tree logic)に興味をお持ちの方に対しては、本講義の中にこの論理の紹介およびマルチエージェントへの応用などが含まれており特に有用であると思います。また、この連続講演の一部は、Ali Mili先生のソフトウェア工学関連の連続講演(http://www.nii.ac.jp/en/calendar/2011/1213/) の後に行われるので、１日で２つの講演を連続して聞くことができます。参加のご検討よろしくお願いします。佐藤　健国立情報学研究所および総研大 ========== - Lecture Series: Social Laws for Multi-Agent Systems: Logic and Games Lecturer: Professor Thomas Agotnes, University of Bergen Thomas Agotnes is a professor at the Department of Information Science and Media Studies at the University of Bergen, Norway. Since his PhD in 2004 form University of Bergen, Agotnes has worked and published extensively in multi-agent systems and related areas. In 2009, he won best paper award at AAMAS 2009 on logical analysis of normative systems. Agotnes is an active member of the international multi-agent systems community. He is a member of the board of directors of the European Association for Multi-Agent Systems (EURAMAS), was the general chair of STAIRS 2010, and has served on the program committees of the main conferences and workshops in his field, including the senior program committees of AAMAS and IJCAI. Schdeule Lecture 1: Specifying and verifying state-transition models for multi-agent Systems Place: National Institute of Informatics, Lecture room 2001, 20F Date: 15:30-17:00, December 13, 2011 Lecture 2: Social laws for coordination Place: National Institute of Informatics, Lecture room 2001, 20F Date: 15:30-17:00, December 20, 2011 Lecture 3: Dealing with non-compliance Place: National Institute of Informatics, Lecture room 2001, 20F Date: 15:30-17:00, December 27, 2011 Lecture 4: Coordinating self-interested agents Place: National Institute of Informatics, Lecture room 2001, 20F Date: 15:30-17:00, January 10, 2012 Lecture 5: Social laws design as an optimisation problem, and as a mechanism design problem Place: National Institute of Informatics, Lecture room 2010, 20F Date: 15:30-17:00, January 17, 2012 Lecture 6: Reasoning about social laws Place: National Institute of Informatics, Lecture room 2010, 20F Date: 15:30-17:00, January 24, 2012 Lecture 7: Strategic reasoning under imperfect information Place: National Institute of Informatics, Lecture room 2010, 20F Date: 15:30-17:00, January 31, 2012

1 0

NII Type Theory Workshop
by Makoto Tatsuta 06 Nov '11

06 Nov '11

Sixth NII Type Theory Workshop Date: November 14, 2011, 11:00--17:00 Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/introduce/access1-j.shtml) Program: 11:00--11:30 Takayuki Koai (National Institute of Informatics) Title: Verification of Substitution Theorem Using HOL 11:30--12:00 Mauricio Hernandes (The Graduate University for Advanced Studies) Title: Game theory from a logician perspective 12:00--13:40 Lunch Break 13:40--14:10 Takanori Hida (Kyoto University) Title: A computational interpretation of the axiom of determinacy 14:10--14:40 Makoto Tatsuta (National Institute of Informatics) Title: Non-Commutative Infinitary Peano Arithmetic 14:40--15:00 Tea Break 15:00--16:00 Neil D. Jones (University of Copenhagen) Title: Termination Analysis of the Untyped lambda-Calculus 16:00--17:00 Stefano Berardi (Torino University) Title: A Topology over a set of Knowledge States and a Fixed Point Problem Abstracts: ---------------------------------------------------------------------- Takayuki Koai (National Institute of Informatics) Title: Verification of Substitution Theorem Using HOL Abstract: Substitution Theorem is a new theorem in untyped lambda calculus, which was proved in 2006. This theorem states that for a given lambda term and given free variables in it, the term becomes weakly normalizing when we substitute arbitrary weakly normalizing terms for these free variables, if the term becomes weakly normalizing when we substitute a single arbitrary weakly normalizing term for these free variables. This paper formalizes and verifies this theorem by using higher-order theorem prover HOL. A control path, which is the key notion in the proof, explicitly uses names of bound variables in lambda terms, and it is defined only for lambda terms without bound variables renaming. The lambda terms without bound variable renaming are formalized by using the HOL package based on contextual alpha-equivalence. The verification uses 10119 lines of HOL code and 326 lemmas. This is a joint work with Makoto Tatsuta. ---------------------------------------------------------------------- Mauricio Hernandes (The Graduate University for Advanced Studies) Title: Game theory from a logician perspective Abstract: I intend in this talk to introduce a few concepts in game theory like Nash Equilibrium and Backward-Induction, and then express those ideas with some modal logic. ---------------------------------------------------------------------- Takanori Hida (Kyoto University) Title: A computational interpretation of the axiom of determinacy Abstract: Axiom of determinacy(AD) is a central topic in descriptive set theory and there are a number of research on this axiom. In this talk, we approach to the computational content of negative translation of AD using realizability interpretation due to Berardi, Bezem and Coquand (1998). ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Non-Commutative Infinitary Peano Arithmetic Abstract: Does there exist any sequent calculus such that it is a subclassical logic and it becomes classical logic when the exchange rules are added? The first contribution of this paper is answering this question for infinitary Peano arithmetic. This paper defines infinitary Peano arithmetic with non-commutative sequents, called non-commutative infinitary Peano arithmetic, so that the system becomes equivalent to Peano arithmetic with the omega-rule if the the exchange rule is added to this system. This system is unique among other non-commutative systems, since all the logical connectives have standard meaning and specifically the commutativity for conjunction and disjunction is derivable. This paper shows that the provability in non-commutative infinitary Peano arithmetic is equivalent to Heyting arithmetic with the recursive omega rule and the law of excluded middle for Sigma-0-1 formulas. Thus, non-commutative infinitary Peano arithmetic is shown to be a subclassical logic. The cut elimination theorem in this system is also proved. The second contribution of this paper is introducing infinitary Peano arithmetic having antecedent-grouping and no right exchange rules. The first contribution of this paper is achieved through this system. This system is obtained from the positive fragment of infinitary Peano arithmetic without the exchange rules by extending it from a positive fragment to a full system, preserving its 1-backtracking game semantics. This paper shows that this system is equivalent to both non-commutative infinitary Peano arithmetic, and Heyting arithmetic with the recursive omega rule and the Sigma-0-1 excluded middle. This is a joint work with Stefano Berardi and was presented at CSL 2011. ---------------------------------------------------------------------- Neil D. Jones (University of Copenhagen) Title: Termination Analysis of the Untyped lambda-Calculus Abstract: An algorithm is developed that, given an untyped lambda-expression, can certify that its call-by-value evaluation will terminate. It works by an extension of the ``size-change principle'' earlier applied to first-order programs. The algorithm is sound (and proven so) but not complete: some lambda-expressions may in fact terminate under call-by- value evaluation, but not be recognised as terminating. The intensional power of size-change termination is reasonably high: It certifies as terminating all primitive recursive programs, and many interesting and useful general recursive algorithms including programs with mutual recursion and parameter exchanges, and Colson's ``minimum'' algorithm. Further, the approach allows free use of the Y combinator, and so can identify as terminating a substantial subset of PCF. (joint work with Nina Bohr; in Logical Methods in Computer Science, 2008, Issue 1) ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: A Topology over a set of Knowledge States and a Fixed Point Problem Abstract: We give an abstract formulation of the termination problem for realizer of Heyting Arithmetic plus various subsystem of classical logic. This termination problem is expressed as the existence of a fixed point for a class of continuous maps in a suitable topology. ----------------------------------------------------------------------

1 0

Workshop on Linear Logic (abstracts available)
by Kazushige TERUI 04 Nov '11

04 Nov '11

皆様線型論理関連ワークショップ（１１月７日−１１日、京都大学）について、アブストラクト入りのプログラムが出来上がりましたのでご案内をさせていただきます。 ※１１月９日（水）の懇親会に参加希望の方は７日（月）までにお申し込みください。 -------------------- Workshop on Linear Logic (Geometry of Interaction, Traced Monoidal Categories and Implicit Complexity) * Date: 7th - 11th, November (11th reserved for free discussion) * Location: Room 110, Faculty of Science Building No.3, Kyoto University http://www.kyoto-u.ac.jp/en/access/campus/north.htm 京都大学理学部３号館１１０号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_n.htm ※数理解析研究所ではありませんのでご注意ください。 * Workshop Dinner 18:30-, 9th November. Izakaya Anji Fuchomae (Annex) http://www.anji-gr.com/futyoumae/index.html 　Students 3,000yen, Others 5,000yen ※Please inform us by 7th Monday if you would like to participate. * Organizers Michele Basaldella: mbasalde(a)kurims.kyoto-u.ac.jp Kazushige Terui: terui(a)kurims.kyoto-u.ac.jp Claudia Faggian * Program with abstracts http://www.kurims.kyoto-u.ac.jp/~terui/wsprogram.pdf ------------------------------------- Registration Form 1. Your name, affiliation, status 2. You participate in the workshop during ?th - ?th November. 3. You do/do not participate in the social dinnter on 9th. 　 (Inform us if you have any dietary option.) -------------------------------------- ------------------------------------------ Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui(a)kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/

1 0

WST 2012: First Call For Papers
by Nao Hirokawa 04 Nov '11

04 Nov '11

来年2月に行われます停止性に関するワークショップの論文投稿募集の案内をお送り致します。今年はオーストリアのオーバーグルグルで開催されます。投稿を見当して頂けますと幸いです。廣川　直（北陸先端科学技術大学院大学） ====================================================================== First Call for Papers WST 2012 12th International Workshop on Termination Feb 19 - 23, 2012, Obergurgl, Innsbruck http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/ ====================================================================== The goal of the Workshop on Termination is to be a venue for presentation and discussion of all topics in and around termination. In this way, the workshop tries to bridge the gaps between different communities interested and active in research in and around termination. We will work very hard to attain the same friendly atmosphere as in past workshops, which enabled fruitful exchanges leading to joint research and subsequent publications. IMPORTANT DATES: * submission December 18, 2012 * notification January 15, 2012 * final version January 29, 2012 * workshop February 19 - 23, 2012 TOPICS: The 12th International Workshop on Termination welcomes contributions on all aspects of termination and complexity analysis. Contributions from the imperative, constraint, functional, and logic programming communities, and papers investigating applications of complexity or termination (for example in program transformation or theorem proving) are particularly welcome. Areas of interest to the workshop include, but are not limited to, the following: * Termination of programs * Termination of rewriting * Termination analysis of transition systems * Complexity of programs * Complexity of rewriting * Implicit computational complexity * Implementations of termination and complexity analysis methods * Certification of termination and complexity proofs * Termination orders, well-founded orders, and reduction orders * Termination methods for theorem provers * Strong and weak normalization of lambda calculi * Termination analysis for different language paradigms * Challenging termination problems/proofs * Applications to program transformation and compilation * Other applications of termination methods * Comparisons and classification of termination methods * Non-termination and loop detection * Termination in distributed systems * Proof methods for liveness and fairness * Well-quasi-order theory * Ordinal notations * Subrecursive hierarchies PROGRAM COMMITTEE: * Ugo Dal Lago University of Bologna * Danny De Schreye K.U. Leuven * Samir Genaim The Complutense University * Nao Hirokawa JAIST * Georg Moser University of Innsbruck (chair) * Albert Rubio Universitat Politecnica de Catalunya * Peter Schneider-Kamp University of Southern Denmark * Rene Thiemann University of Innsbruck SUBMISSION: Submissions are short papers/extended abstract which should not exceed 5 pages. There will be no formal reviewing. The accepted papers will be made available electronically before the workshop. Papers should be submitted electronically via the submission page: http://www.easychair.org/conferences/?conf=wst2012 Final versions should be created using LaTeX and the style file LIPIcs (http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz).

1 0

数学基礎論若手の会 (3rd announcement)
by SAKAI Hiroshi 01 Nov '11

01 Nov '11

皆様：神戸大学の酒井拓史と申します．数学基礎論若手の会のご案内をさせていただきます．今年度の数学基礎論若手の会の申し込み締め切りが 11月6日(日) と迫っていますが，いまのところ参加枠と講演枠にかなりの余裕があります．皆様のふるってのご参加／ご講演をお待ちしています．また，お近くに数学基礎論を勉強している学生さんや，興味をお持ちの方がいらっしゃいましたら，周知していただけると助かります．よろしくお願いします．以下は，以前にも当メーリングリストに配信させていただいた若手の会の案内です：数学基礎論若手の会は，数学基礎論を専攻する学生と若手研究者の交流を目的とした，合宿形式の研究集会です．これから数学基礎論を勉強しようとしている学生さんの参加なども歓迎します．また講演はオリジナルの成果発表の他にも，研究の途中報告や内容紹介など幅広く募集しています．過去の若手の会の記録は以下のページでご覧いただけます： http://www.mi.s.osakafu-u.ac.jp/~kada/wakate/index.html 今年度の若手の会は下記の要領で開催します．ご質問等ありましたら，幹事の酒井までお気軽にご連絡ください．日程： 12月9日(金)午後〜 11日(日)午前場所：大阪府羽衣青少年センター http://www.osaka-yha.com/osakakokusai/ 幹事：酒井拓史 (神戸大学) hsakai(a)people.kobe-u.ac.jp ホームページ： http://www2.kobe-u.ac.jp/~hsakai/wakate2011/ [宿泊・食事] 宿泊と食事は会場併設の大阪国際ユースホステルを利用します．宿泊は12月9日(金)と10日(土)の2晩，食事は9日(金)の夕食から 11日(日)の朝食までの5食を下記料金で利用いただけます：宿泊： 1人1泊 2,800円 (6人部屋利用) 食事：朝食 630円，昼食 630円，夕食 1,050円 ※ 個室などを希望される方は，お早めに酒井までご連絡ください． ※ 夕食後に親睦会を予定しており，会費を別途 1,000円程度いただく予定です． [参加申し込み] 参加を希望される方は，幹事の酒井にメールにてお申し込みください． <申込締切> 11月6日(日) =========== 参加申し込みフォーム ============ 氏名：所属：職名・学年：参加希望日程：全日程参加 or ... 講演希望：希望する or 希望しない or 未定講演タイトル： (未定の場合は "未定" とご記入ください．) 講演時間： 30分程度 or 60分程度 or 未定宿泊： 9日(金)の夜 … ○ or × 10日(土)の夜 … ○ or × 食事： 9日(金)夕食 … ○ or × 10日(土)朝食 … ○ or × 10日(土)昼食 … ○ or × 10日(土)夕食 … ○ or × 11日(日)朝食 … ○ or × 質問・要望等： ============================================== 多くの方のご参加・ご講演をお待ちしております． --------------------------------------------- 酒井拓史神戸大学大学院システム情報学研究科講師 e-mail: hsakai(a)people.kobe-u.ac.jp tel: 078-803-245 address: 〒657-8501 神戸市灘区六甲台町 1-1 神戸大学システム情報学研究科 ---------------------------------------------

1 0

Talk by Michele Basaldella, Tue 1 Nov at RIMS, Kyoto U
by Kenshi Miyabe 24 Oct '11

24 Oct '11

数理解析研究所　特定研究員の宮部です。重複して受け取られた場合はご容赦ください． RIMSでは、2週間に1度、GCOE tea timeを行っています。 http://www.kurims.kyoto-u.ac.jp/~kenkyubu/gcoe/2008teatime.html 来週、2011年11月1日(火)、第48回 GCOE tea timeでは、 Micheleが話をします。時間のご都合がよろしければ是非ご参加ください．講演者： Michele BASALDELLA (数理解析研究所　研究員) タイトル: Dilators: a gentle introduction 講演の概要: We aim to recall some basic aspects of the concept of dilator, a notion which has been introduced in proof-theory (a branch of mathematical logic) by J.-Y. Girard about 30 years ago. Essentially, a dilator is a certain kind of endofunctor of the category of the ordinal　numbers, which can be thought as an abstract counterpart of the more concrete system of ordinal notation which are abundant in proof-theory. In this introductory talk, we recall the notion of denotation system (a kind of generalization of the Cantor normal form representation of the ordinal numbers), the notion of dilator, and show a correspondence between them. なお、この講演は英語で行われます。時間(Time)：15:00-16:00 場所(Place)：数理解析研究所402号室(RIMS, Room 402) -- Kenshi Miyabe email: kmiyabe(a)kurims.kyoto-u.ac.jp Researcher Research Institute for Mathematical Sciences, Kyoto University Kyoto 606-8502 Japan Tel: +81-75-753-7202 / Fax: +81-75-753-7272

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml