Logic-ml November 2011

logic-ml@fos.kuis.kyoto-u.ac.jp

12 participants
13 discussions

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

26 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 25 Nov '11

25 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 25 Nov '11

25 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 17 Nov '11

17 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 16 Nov '11

16 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 16 Nov '11

16 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 09 Nov '11

09 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 08 Nov '11

08 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 07 Nov '11

07 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 07 Nov '11

07 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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml November 2011