Logic-ml

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

1792 discussions

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

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml