Logic-ml June 2015

16 participants
19 discussions

セミナー案内
by KASHIMA Ryo 17 Nov '15

17 Nov '15

数理論理学セミナーのお知らせ日時：1月23日(金) 16:00から場所：東京工業大学大岡山西８号館Ｗ棟10階 W1008 話者：鈴木信行（静岡大学）題目：中間述語論理におけるExistence Propertyに関する話題 --- 小野の問題P52とその周辺 --- 概要：始めに中間述語論理の簡単な紹介をします。ざっくり言うと、中間述語論理とは、直観主義述語論理と古典述語論理の「中間」にある述語論理です。つぎに、existence property と disjunction property と言う性質を考えます。これらは、直観主義論理の構成性(constructivity)を示す顕著な性質として知られています。中間述語論理の枠組みでこれらを考察してみると、この2つの性質が独立であることが解ります。これは、小野の問題P52として知られる問題に否定的解決を与えます。今回は、これにまつわる若干のことがらも報告したいと思います。 ------ 本セミナーは定期的に東工大で開催しているものです。初めて参加を希望される方はご一報ください。 ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp

1 3

JAIST Logic Seminar Series
by Hajime Ishihara 05 Sep '15

05 Sep '15

皆様ジーゲン大学のDieter Spreen先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * This seminar is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project COMPUTAL (http://computal.uni-trier.de/). Date: Thursday 7 May, 2015, 13:30-15:00 Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Dieter Spreen (University of Siegen) Title: Digit Spaces - Topological Foundations Abstract: Digit spaces have been introduced by Ulrich Berger as a framework for extracting programs that deal with continuous data from formal proofs. The essential idea was to represent objects as streams of unary contractions on a complete metric space and to use coinduction on the logical side. In recent joint work on an extension of this approach to hyperspaces like the space of nonempty compact subsets of a digit space, it turned out that compact cannot be represented by such streams in general: instead one has to deal with infinite trees the nodes of which are labeled by contraction similar to the stream case. It was realized, however, that one will obtain a uniform theory, if the contractions, also called digits, are allowed to be multi-ary.

2 2

CFP: Ninth International Workshop on Juris-informatics (JURISIN 2015)
by Ken Satoh 28 Aug '15

28 Aug '15

Call for Papers Ninth International Workshop on Juris-informatics (JURISIN 2015) http://research.nii.ac.jp/~ksatoh/jurisin2015 associated with JSAI International Symposia on AI 2015 (IsAI-2015) https://www.ai-gakkai.or.jp/isai/ Date: November 16 - 18, 2015 Place: Raiosha Building, Keio University Kanagawa, Japan http://www.keio.ac.jp/en/maps/hiyoshi.html Aims and Scope Juris-informatics is a new research area which studies legal issues from the perspective of informatics. The purpose of this workshop is to discuss both the fundamental and practical issues among people from the various backgrounds such as law, social science, information and intelligent technology, logic and philosophy, including the conventional "AI and law" area. We solicit unpublished papers on theories, technologies and applications on juris-informatics. Important Dates Submission Deadline: August 28, 2015 Notification October 1, 2015 Camera-ready due October 15, 2015 Workshop: November 16 - 18, 2015 Topics Relevant topics include, but are not limited to, the following: * Model of legal reasoning * Argumentation / Negotiation / Argumentation agent * Legal term ontology * Formal legal knowledge-base / Intelligent management of legal knowledge-base * Translation of legal documents * Information retrieval of legal texts * Computer-aided law education * Use of Informatics and AI in law * Legal issues on ubiquitous computing / multi-agent system / the Internet * Social implications of use of informatics and AI in law * Natural language processing for legal knowledge * Verification and validation of legal knowledge systems * Any theories and technologies which is not directly related with juris-informatics but has a potential to contribute to this domain Bar Exam Competition JURISIN invites participation in a legal information extraction and entailment competition. Previous conferences/workshops have not conducted such a shared task on a large legal data collection, so we hope that the 2015 workshop will help establish a major experimental effort in the legal information extraction/retrieval field. The motivation for the competition is to help create a research community of practice for the capture and use of legal information. Please visit the homepage of the bar exam competition: "http://webdocs.cs.ualberta.ca/~miyoung2/COLIEE2015/" Invited Speakers Giovanni Sartor (University of Bologna/European University Institute of Florence) Phan Minh Dung (Asian Institute of Technology, Thailand, (under negotiation)) Submissions We welcome and encourage the submission of high quality, original papers, which are not simultaneously submitted for publication elsewhere except as a submission to JURIX 2015 (The 28th International Conference on Legal Knowledge and Information Systems) "http://jurix2015.di.uminho.pt/". The double submission policy with JURIX 2015 is as follows: 1. Papers being submitted both to JURISIN2015 and JURIX2015 must note this on the title page. 2. A paper to be presented at JURISIN2015 must be withdrawn from JURIX2015 and vice versa according to the choice by the authors. 3. If the authors do not follow this double submission policy, the paper by the authors will not be included in the proceedings of JURISIN 2015. Papers should be written in English, formatted according to the Springer Verlag LNCS style in a pdf form, which can be obtained from "http://www.springeronline.com" and not exceed 14 pages including figures, references, etc. If you use a word file, please follow the instruction of the format, and then convert it into a pdf form and submit it at the paper submission page. If a paper is accepted, at least one author of the paper must register the workshop and present it. Please submit a paper at "https://easychair.org/conferences/?conf=jurisin2015". Post Proceedings We are under negotiation with Springer Verlag for publication of Post Proceedings as the preivous arragements. Workshop Chairs Takehiko Kasahara, Toin Yokohama University, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Steering Committee Members Takehiko Kasahara, Toin Yokohama University Makoto Nakamura, Nagoya University, Japan Katsumi Nitta, Tokyo Institute of Technology, Japan Seiichiro Sakurai, Meiji Gakuin University, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Satoshi Tojo, Japan Advanced Institute of Science and Technology(JAIST), Japan Katsuhiko Toyama, Nagoya University, Japan Advisory Committee Members Trevor Bench-Capon, The University of Liverpool, UK Tomas Gordon, Fraunfoher FOKUS, Germany Henry Prakken, University of Utrecht & Groningen, The Netherlands John Zeleznikow, Victoria University, Australia Robert Kowalski, Imperial College London, UK Kevin Ashley, University of Pittsburgh, USA Program Committee Members Thomas Agotnes, University of Bergen, Norway Katie Atkinson, University of Liverpool, UK Marina De Vos,University of Bath, UK Randy Goebel, University of Alberta, Canada Guido Governatori, NICTA, Australia Tokuyasu Kakuta, Nagoya University, Japan Yoshinobu Kano, Shizuoka University, Japan Takehiko Kasahara, Toin Yokohama University, Japan Mi-Young Kim, University of Alberta, Canada Robert Kowalski, Imperial College London, UK Masahiro Kozuka, Okayama University, Japan Nguyen Le Minh, Japan Advanced Institute of Science and Technology(JAIST), Japan Beishui Liao, Zhejiang University, China Minghui Ma, Southwest University, China Makoto Nakamura, Nagoya University, Japan Katumi Nitta, Tokyo Institute of Technology, Japan Paulo Novais, University of Minho, Portugal Antonino Rotolo, University of Bologna, Italy Seiichiro Sakurai, Meiji Gakuin University, Japan Katsuhiko Sano, Japan Advanced Institute of Science and Technology(JAIST), Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Akira Shimazu, Japan Advanced Institute of Science and Technology(JAIST), Japan Hirotoshi Taira, Osaka Institute of Technology, Japan Fumihiko Takahashi, Meiji Gakuin University, Japan Satoshi Tojo, Japan Advanced Institute of Science and Technology(JAIST), Japan Katsuhiko Toyama, Nagoya University, Japan Minghui Xiong, Sun Yat-sen University, China Baosheng Zhang, China University of Political Science and Law, China Previous JURISIN workshops * JURISIN2007 <http://research.nii.ac.jp/%7Eksatoh/jurisin.html> * JURISIN2008 <http://www.ntt.dis.titech.ac.jp/jurisin2008/> * JURISIN2009 <http://research.nii.ac.jp/%7Eksatoh/jurisin2009.html> * JURISIN2010 <http://research.nii.ac.jp/%7Eksatoh/jurisin2010.html> * JURISIN2011 <http://research.nii.ac.jp/%7Eksatoh/jurisin2011.html> * JURISIN2012 <http://www.kl.i.is.nagoya-u.ac.jp/jurisin2012/> * JURISIN2013 <http://www.ntt.dis.titech.ac.jp/jurisin2013/> * JURISIN2014 <http://www.jaist.ac.jp/org/jurisin2014/> For any inquiry concerning the workshop, please send it to "ksatoh[at]nii.ac.jp"

1 1

NLCS'15 Program
by Makoto Kanazawa 30 Jun '15

30 Jun '15

*********************** Call for Participation *********************** Third Workshop on Natural Language and Computer Science NLCS '15 July 5, 2015 Kyoto, Japan http://www.indiana.edu/~iulg/nlcs.html Program with abstracts: http://easychair.org/smart-program/NLCS'15/index.html Venue: Kyoto University, Clock Tower Centennial Hall, 2nd Floor, Conference Room 3 http://www.kurims.kyoto-u.ac.jp/icalp-lics2015/workshops.html Schedule: 10:30-11:00 Coffee Break 11:00-12:30 Session 1 11:00 Makoto Kanazawa, Distributional Learning of Formal Languages: A Logic-Based Approach (invited talk) 12:00 Philippe de Groote, On Logical Relations and Conservativity 12:30-14:00 Lunch Break 14:00-15:30 Session 2 14:00 Bruno Mery, Lexical Semantics with Linear Types 14:30 Gabriel Gaudreault, Bidirectional Functional Semantics for Pregroup Grammars 15:00 Glyn Morrill and Oriol Valentín, Computational Coverage of TLG: Nonlinearity 15:30-16:00 Coffee Break 16:00-17:00 Session 3 16:00 Gerard de Melo, Learning to Reason about the World using Big Data (invited talk) 17:00-17:15 Short Break without Coffee 17:15-18:15 Session 4 17:15 Oleg Kiselyov, Applicative Abstract Categorial Grammar 17:45 Sylvain Salvati, Non-linear Second Order Abstract Categorial Grammars and Deletion ------------------------------------- Contact: Makoto Kanazawa

1 0

モデル理論夏の学校（講演申込み締切）
by ikeda＠hosei.ac.jp 27 Jun '15

27 Jun '15

皆様，以前，メールいたしました「モデル理論夏の学校」に関して，講演（および参加）申込み締切を７月１１日に延長しました．講演予定でまだ申込みをされていない方は申込みの手続き，よろしくお願いいたします．池田宏一郎（法政大学） ------------------------------------------------------------------ 皆様，法政大学の池田と申します．今年８月に法政大学で研究集会「モデル理論夏の学校2015」が開催されます．この研究集会は毎年夏に開催されるモデル理論および関連分野に関する研究集会です．モデル理論に興味のある方の参加をお待ちしております．・日程：２０１５年８月２２日（土）- ２４日（月）・会場：法政大学市ヶ谷キャンパス５５年館５５１教室・所在地：〒102-8160東京都千代田区富士見2-17-1 ・世話人：池田宏一郎（法政大学経営学部，ikeda(at)hosei.ac.jp）・Web page：https://sites.google.com/site/modeltheorysummer2015/ 参加を希望される方は，下記のフォームに必要事項を記入の上，池田宛に電子メールでお申し込みください．なお，旅費補助は講演者を優先に考えております． %%%%%%%%%%モデル理論夏の学校・参加申し込みフォーム%%%%%%%%%% ・氏名：・所属機関：・職名／学年：・講演：する／しない・講演題目：・旅費補助の希望：する／しない %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 池田宏一郎（法政大学）

2 1

千葉 logic seminar (2015年7月8日)
by Naohi Eguchi 24 Jun '15

24 Jun '15

千葉 logic seminar の第6回のお知らせです。どなたでも参加できますのでどうぞ気軽にいらっしゃって下さい。問合せ先江口（千葉大学） Naohi Eguchi <neguchi(a)g.math.s.chiba-u.ac.jp> --------------------------------------- 千葉 Logic Seminar https://sites.google.com/site/chibalogicseminar/home/seminar 日時：2015年7月8日(水)15:00-16:00 場所：千葉大学理学部2号館105号室アクセスは http://www.chiba-u.ac.jp/campus_map/nishichiba/index.html の地図の黄色い理学部の中で数字2が付いている建物の1階です。 Speaker: Martin Avanzini (University of Innsbruck) Title: Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order Abstract: In this talk I will outline the content of our recent ICFP paper. Here, we shows how the runtime complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalized versions of them, and feeding the result to existing tools for the complexity analysis of first-order term rewrite systems. Crucial, all involved transformations are complexity reflecting. As a consequence, a complexity certificate on the first-order system can be relayed back (asymptotically) to the initial higher-order program. Reference: Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order Martin Avanzini, Ugo Dal Lago and Georg Moser Proc. ICFP 2015, to appear. Long version: http://arxiv.org/abs/1506.05043

1 0

Klaus Keime 教授講演会
by Hideki Tsuiki 23 Jun '15

23 Jun '15

京都大学人間・環境学研究科の立木です。 7 月 3 日 (LICS サテライト Workshop の前日) に、Darmstadt 工科大学の Klaus Keimel 先生による講演会を京都大学で行います。どうぞ、お気軽にお越しください。講演会の後に、一緒にお食事に行こうと考えています。人数を把握しておきたいので、お食事に来られる方は、あらかじめメールでご連絡頂けると幸いです。多くの方のご参加をお待ちしております。立木 ------------------------------------------------------------ 講演会のお知らせ日時： 7月3日（金） 16:30 より場所：京都大学総合人間学部棟 1401 教室 (吉田南キャンパスに入って左側の建物の４Fです）講演者： Klaus Keimel (Darmstadt 工科大学名誉教授) 題目： On the equivalence of state transformer semantics and predicate transformer semantics The meaning of a program may be modeled by the input-output behavior, we call it 'state transformer semantics'. Alternatively, for verifying programs one will be interested in properties A of the output and one wants to find conditions on the input that guarantee property A for the output. One will work with the transformation that assigns to property A of the output the weakest precondition p(A) on the input that guarantees property A for the output; let us call it 'predicate transformer semantics'. In the presence of computational effects like nondeterministic or probabilistic choice, a computation will not be modeled by a function that transforms inputs from a input domain X to an output domain Y but by a state transformer t:X --> T(Y), where T is an appropriate computational monad. The corresponding predicate transformer p associates predicates on Y to predicates on X. Not all predicate transformers will correspond to state transformers, and one looks for necessary and, if possible, sufficient conditions for predicate transformers to correspond to state transformers t:X --> T(Y). Such conditions are sometimes called 'healthiness' conditions. Most examples in the literature dealing with the equivalence of the two semantics can be seen to be based on a domain R of 'observations' and a monad T 'subordinate' to the continuation monad [[(-) --> R] --> R]. For the continuation monad predicates on objects X take values in R. For the continuation monad the state transformers t and the predicate transformers p corresponding to another are related by 'swapping arguments': t(x)(A)= p(A)(x) for x in X and predicates A on Y. It is the aim of this paper to describe a framework of an algebraic/order theoretical nature for the monad T so that the equivalence between state and predicate transformer semantics described above for the continuation monad can be carried over. This framework always yields necessary healthiness conditions. The sufficiency criterion has to be verified in each special situation separately. We illustrate our methods by several examples. As semantic domains we use dcpos (directed complete partially ordered sets). But the same methods can be applied to other Cartesian closed categories and beyond, as we indicate in the concluding remarks.

1 0

Sylvain Salvati at NII Logic Seminar 7/1
by Makoto Kanazawa 23 Jun '15

23 Jun '15

Lecture by Sylvain Salvati at NII Logic Seminar Date and Time: July 1, 16:00-17:00 Place: National Institute of Informatics, Conference Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Sylvain Salvati (INRIA Bordeaux Sud-Ouest) Title: Model construction for higher-order model-checking Abstract: When dealing with finite state properties, it is usual to have some finite algebraic structures (e.g. finite monoids in the case of finite state automata on strings) that represent those properties. When dealing with logical properties of programs that are computed by finite state automaton, the question of what is an "adequate" finite algebraic structure arises. Having such a structure would entail a sort of modularity in program verification, but it also gives some strong understanding of how the properties can be checked. In the context of higher-order verification, programs are models as lambda-terms and it is natural to think about denotational domains as a possible candidate. Finitary Scott domains only capture very simple properties of the Bohm trees generated by higher-order programs. This talk will illustrate how to enrich Scott domains so that they can capture wider classes of finite state properties. 問合せ先: 金沢誠 (国立情報学研究所) e-mail: kanazawa(a)nii.ac.jp

1 0

CTFM2015 Call for abstracts
by YOKOYAMA Keita 20 Jun '15

20 Jun '15

皆様、北陸先端大の横山です。締め切りが近づきましたので、下記の研究集会の情報を再送致します。横山啓太 ---------- Forwarded message ---------- From: YOKOYAMA Keita <y-keita(a)jaist.ac.jp> Date: 2015-05-14 22:49 GMT-07:00 Subject: Fwd: CTFM2015 Call for abstracts To: logic-ml(a)fos.kuis.kyoto-u.ac.jp, kisoron-ml(a)fos.kuis.kyoto-u.ac.jp ****************************** 以下の要領で研究集会 Computability Theory and Foundations of Mathematics 2015 (2015年9月7日(月)～9月11日(金)，東京工業大学大岡山キャンパス) を開催いたします．詳しい情報については、下記のホームページをご覧ください。 http://www.jaist.ac.jp/CTFM/CTFM2015/index.html 講演の募集の締め切りは6月15日となっております。また、講演受理の連絡は6月25日までにお送りする予定です。宜しく参加・講演をご検討ください。 ============================================================ Computability Theory and Foundations of Mathematics (Tokyo Institute of Technology, Tokyo, Japan, September 7-11, 2015) http://www.jaist.ac.jp/CTFM/CTFM2015/index.html ============================================================ Computability Theory and Foundations of Mathematics (CTFM) aims to develop computability theory and logical foundations of Mathematics. The scope involves the topics Computability Theory, Reverse Mathematics, Nonstandard Analysis, Proof Theory, Set Theory, Philosophy of Mathematics, Constructive Mathematics, Theory of Randomness and Computational Complexity Theory. In honor of Professor Kazuyuki Tanaka's 60th birthday, this year's conference will include sessions covering areas in which Professor Tanaka has worked. This conference is held jointly with a workshop of Bilateral Joint Research Project sponsored by the Japan Society for the Promotion of Science and the National University of Singapore. See the previous workshop on this project JSPS-NUS Joint Workshop in Mathematical Logic and Foundations of Mathematics (March 6 - 8, 2015, Kanazawa, Japan). This is the fifth conference of CTFM conference series. See also the last year conference Computability Theory and Foundations of Mathematics 2014 (February 17 - 20, 2014, Tokyo, Japan). -------------------------------------------- Submission deadline for Presentations: June 15, 2015 -------------------------------------------- Invited Speakers Ali Enayat (University of Gothenburg) Sy Friedman (Kurt Gödel Research Center) Alberto Marcone (The University of Udine) Nik Weaver (Washington University) Guohua Wu (Nanyang Technological University) Stephen Binns (King Fahd University of Petroleum and Minerals) Liang Yu (Nanjing University) Sakae Fuchino (Kobe University) Joel Hamkins (City University of New York) Dilip Raghavan (National University of Singapore) Hidenori Kurokawa (Kobe University) Kengo Okamoto (Tokyo Metropolitan University) Toshio Suzuki (Tokyo Metropolitan University) Tin Lok Wong (Kurt Gödel Research Center) -------------------------------------------- Programme Committee Chi Tat Chong (National University of Singapore, co-chair) Kojiro Higuchi (Chiba University) Makoto Kikuchi (Kobe University) Takako Nemoto (JAIST) Stephen G. Simpson (Pennsylvania State University, co-chair) Toshimichi Usuba (Kobe University) Andreas Weiermann (Ghent University) Takeshi Yamazaki (Tohoku Universigy) Yang Yue (National University of Singapore) Keita Yokoyama (JAIST / UC Berkeley) -------------------------------------------- Organising Committee Makoto Fujiwara (JAIST) Ryo Kashima (Tokyo Institute of Technology, local chair) Takayuki Kihara (UC Berkeley) Takako Nemoto (JAIST) Florian Pelupessy (Tohoku University) Takeshi Yamazaki (Tohoku University, co-chair) Keita Yokoyama (JAIST / UC Berkeley, co-chair) -------------------------------------------- どうぞよろしくお願い致します。横山啓太 -- Keita Yokoyama y-keita(a)jaist.ac.jp

1 1

Talk by Matthew de Brecht (25 Jun 11:00-)
by Tetsuya Sato 19 Jun '15

19 Jun '15

京都大学数理解析研究所の佐藤です。 6月25日11:00から、情報通信研究機構・脳情報通信融合研究センターの Matthew de Brecht氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 25 Jun, 2015 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Matthew de Brecht (NICT, CiNet) Title: Towards a descriptive set theory for QCB spaces. Abstract: QCB spaces (quotients of countably based spaces) are a convenient cartesian closed category of topological spaces with important applications in computable analysis and for modeling the semantics of programming languages. However, they generally fail to be countably based and have very complicated topologies, which so far has been a major obstacle for obtaining a deep understanding of these spaces. In this talk, I will present recent joint work with M. Schroeder and V. Selivanov concerning a classification of QCB0 spaces according to the descriptive complexity of defining a basis for their topologies. Our approach provides useful tools for analyzing when one QCB space can be embedded into another, and has deep connections with the projective hierarchy from descriptive set theory. We will present some applications concerning the existence of universal QCB-spaces, as well as some results on the Kleene-Kreisel continuous functionals.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml June 2015