Logic-ml May 2016

11 participants
14 discussions

4th AJSW = 45th TRS Meeting
by Nao Hirokawa 03 May '16

03 May '16

皆様今年９月に開催される「第45回 TRS Meeting」参加者募集をご案内致します。通常、国内で開催しておりますが、今回は項書換えに関する日墺のサマーワークショップとして、オーストリアのオーバーグルグルで開催されます。皆様、ぜひ参加をご検討下さい。廣川直 (JAIST) ====================================================================== 4th Austria-Japan Summer Workshop on Term Rewriting 45th TRS Meeting Obergurgl http://cl-informatik.uibk.ac.at/events/ajsw-2016/ AJSW is an informal workshop for researchers in Austria and Japan and aims to facilitate and share new developments and ideas in term rewriting. Not only presentations about published results but also work-in-progress talks are welcome. The event is held as part of CLA 2016 http://cl-informatik.uibk.ac.at/events/cla-2016/ and synonymous with the 45th TRS Meeting. The Term Rewriting Meeting (TRS Meeting) is a biannual informal workshop that aims at promoting the research on rewriting and related areas. Participants are expected to give a talk of approximately 15 to 60 minutes in English on their research activities. The subject of the talk is not required to be one's original result; for example, explaining an interesting paper is perfectly acceptable. (For information on TRS meetings in general, see: http://www.jaist.ac.jp/~hirokawa/trs-meeting/) Date: September 7 (Wed) -- 9 (Fr), 2013 Venue: Obergurgl University Center http://www.uz-obergurgl.at/english/ Gaisbergweg 5, 6456 Obergurgl, Austria Program September 7 (Wed) CLA excursion September 8 (Thu) first day of workshop September 9 (Fri) second day of workshop Preliminary Registration Please indicate whether you would like to join by sending the registration form below to Christian Sternagel (christian.sternagel(a)uibk.ac.at) as soon as possible. This is just in order to get a rough estimate of the number of participants. The official registration and arrangements for accommodation will be handled through the main CLA 2016 event. ---------------------------------------------------------------------- Registration Form of the 45th TRS Meeting name: affiliation: number of accompanying persons: attendance: CLA / AJSW + excursion / AJSW only ---------------------------------------------------------------------- * number of accompanying persons: in case you want to bring family and/or significant others (which is encouraged), please indicate the number of additional persons here * CLA: full week, arrival on September 4 (Sun) and departure on September 10 (Sat); this is the preferred option * AJSW + excursion: arrival on September 6 (Tue) and departure on September 10 (Sat) * AJSW only: arrival on September 7 (Wed) and departure on September 10 (Sat)

1 0

【投稿〆切せまる：概要5/9，論文5/16】CFP: PPDP2016
by Kazutaka Matsuda 02 May '16

02 May '16

logic-ml関係者の皆様，東北大学の松田です．複数受け取られた場合はご容赦ください．投稿〆切が近付いてまいりましたので，イギリスのエジンバラにて9/5〜9/7で開催されます宣言的プログラミングに関する国際会議 PPDP 2016 の論文募集のご案内を再度お送りいたします．投稿〆切はアブストラクト：　5月9日論文：　　　　　　5月16日となっております．どうぞ論文の投稿をご検討いただけますと幸いです． ====================================================================== Second call for papers 18th International Symposium on Principles and Practice of Declarative Programming PPDP 2016 Special Issue of Science of Computer Programming (SCP) Edinburgh, UK, September 5-7, 2016 (co-located with LOPSTR and SAS) http://ppdp16.webs.upv.es/ ====================================================================== SUBMISSION DEADLINE: 9 MAY (abstracts) / 16 MAY (papers) ---------------------------------------------------------------------- INVITED SPEAKERS Elvira Albert, Complutense University of Madrid, Spain ---------------------------------------------------------------------- PPDP 2016 is a forum that brings together researchers from the declarative programming communities, including those working in the logic, constraint and functional programming paradigms, but also embracing languages, database languages, and knowledge representation languages. The goal is to stimulate research in the use of logical formalisms and methods for specifying, performing, and analyzing computations, including mechanisms for mobility, modularity, concurrency, object-orientation, security, verification and static analysis. Papers related to the use of declarative paradigms and tools in industry and education are especially solicited. Topics of interest include, but are not limited to * Functional programming * Logic programming * Answer-set programming * Functional-logic programming * Declarative visual languages * Constraint Handling Rules * Parallel implementation and concurrency * Monads, type classes and dependent type systems * Declarative domain-specific languages * Termination, resource analysis and the verification of declarative programs * Transformation and partial evaluation of declarative languages * Language extensions for security and tabulation * Probabilistic modeling in a declarative language and modeling reactivity * Memory management and the implementation of declarative systems * Practical experiences and industrial application This year the conference will be co-located with the 26th Int'l Symp. on Logic-Based Program Synthesis and Transformation (LOPSTR 2016) and the 23rd Static Analysis Symposium (SAS 2016). The conference will be held in Edinburgh, UK. Previous symposia were held at Siena (Italy), Canterbury (UK), Madrid (Spain), Leuven (Belgium), Odense (Denmark), Hagenberg (Austria), Coimbra (Portugal), Valencia (Spain), Wroclaw (Poland), Venice (Italy), Lisboa (Portugal), Verona (Italy), Uppsala (Sweden), Pittsburgh (USA), Florence (Italy), Montreal (Canada), and Paris (France). You might have a look at the contents of past PPDP symposia, http://sites.google.com/site/ppdpconf/ Papers must describe original work, be written and presented in English, and must not substantially overlap with papers that have been published or that are simultaneously submitted to a journal, conference, or workshop with refereed proceedings. Work that already appeared in unpublished or informally published workshop proceedings may be submitted (please contact the PC chair in case of questions). After the symposium, a selection of the best papers will be invited to extend their submissions in the light of the feedback solicited at the symposium. The papers are expected to include at least 30% extra material over and above the PPDP version. Then, after another round of reviewing, these revised papers will be published in a special issue of SCP with a target publication date by Elsevier of 2017. Important Dates Abstract submission: 9 May, 2016 Paper submission: 16 May, 2016 Notification: 20 June, 2016 Final version of papers: 17 July, 2016 Symposium: 5-7 September, 2016 Authors should submit an electronic copy of the full paper in PDF. Papers should be submitted to the submission website for PPDP 2016. Each submission must include on its first page the paper title; authors and their affiliations; abstract; and three to four keywords. The keywords will be used to assist the program committee in selecting appropriate reviewers for the paper. Papers should consist of the equivalent of 12 pages under the ACM formatting guidelines. These guidelines are available online, along with formatting templates or style files. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should include a clear identification of what has been accomplished and why it is significant. Authors who wish to provide additional material to the reviewers beyond the 12-page limit can do so in clearly marked appendices: reviewers are not required to read such appendices. Program Committee Sandra Alves, University of Porto, Portugal Zena M. Ariola, University of Oregon, USA Kenichi Asai, Ochanomizu University, Japan Dariusz Biernacki, University of Wroclaw, Poland Rafael Caballero, Complutense University of Madrid, Spain Iliano Cervesato, Carnegie Mellon University Marina De Vos, University of Bath, UK Agostino Dovier, Universita degli Studi di Udine, Italy Maribel Fernandez, King's College London, UK John Gallagher, Roskilde University, Denmark, and IMDEA Software Institute, Spain Michael Hanus, CAU Kiel, Germany Martin Hofmann, LMU Munchen, Germany Gerda Janssens, KU Leuven, Belgium Kazutaka Matsuda, Tohoku University, Japan Fred Mesnard, Universite de la Reunion, France Emilia Oikarinen, Finnish Institute of Occupational Health, Finland Alberto Pettorossi, Universita di Roma Tor Vergata, Italy Tom Schrijvers, KU Leuven, Belgium Josep Silva, Universitat Politecnica de Valencia, Spain Perdita Stevens, University of Edinburgh, UK Peter Thiemann, Universitat Freiburg, Germany Frank D. Valencia, CNRS-LIX Ecole Polytechnique de Paris, France, and Pontificia Universidad Javeriana de Cali, Colombia German Vidal, Universitat Politecnica de Valencia, Spain (Program Chair) Stephanie Weirich, University of Pennsylvania, USA Program Chair German Vidal Universitat Politecnica de Valencia Camino de Vera, S/N E-46022 Valencia, Spain Email: gvidal(a)dsic.upv.es Organizing committee James Cheney (University of Edinburgh, Local Organizer) Moreno Falaschi (University of Siena, Italy) ----------------------------------------------------------------------

1 0

ワークショップ「証明論的意味論の最前線」のお知らせ
by Shunsuke Yatabe 01 May '16

01 May '16

皆様このたび、5月8（日）に、東京・慶応大学において、以下の要領で論理学の哲学に関するワークショップを開催することになりましたので、ご案内申し上げます。 ******************************************************************** 応用哲学会WSワークショップ「証明論的意味論の最前線」日時：5月8日（日）15:30-17:30 場所：慶應義塾大学三田キャンパス１０２教室（D会場）応用哲学会2016年度大会において行われます <http://www.jacap.org/events/jacap2016.html> http://www.jacap.org/events/jacap2016.html 発表者：五十嵐涼介、鈴木右京、矢田部俊介ワークショップ証明論的意味論の最前線証明論的意味論は、意味の使用説および推論主義に影響を受け、論理結合子の意味はその導入規則と除去規則によって与えられると考える論理学の哲学上の立場である。通常よく使われるモデル論的な意味論と異なり、推論規則自身が論理結合子の意味を与えるとみなす立場は、計算機科学における帰納的データ型の考え方などと親和性も高く、近年、広く研究されるようになってきた。かつては、ダメットらが証明論的意味論で正当化できるのは直観主義論理であり、その点で直観主義論理は古典論理と比べてアドバンテージを持つと論じていたが、ラムフィットらの古典論理も同じ枠組みで正当化できるのではないかという研究も登場した。同時に、多くの非古典論理の体系についても、この枠組みから意味論を与える研究が行われている。本WS では、この話題に関し、導入的な説明を行うとともに、以下の二つのラムフィットに関連する先端的な研究を紹介し、現在の証明論的意味論研究の最前線と、その哲学的意義を検討する。（１）双側面説・古典論理・否認の価値（鈴木右京） PTS （証明論的意味論）とは、自然演繹における導入規則、及び除去規則を利用して、論理結合子の意味を説明するとともに、一定の論理体系を正当化しようとするプログラムのことを指す。ダメットやプラヴィッツによって唱導されてきた従来型の PTS は、直観主義論理のみを対象としたものであったが、ラムフィットは、従来の主張だけを基礎的言語行為と認めるやり方ではなく、否認も文の意味決定に参入する双側面説の立場を取れば、古典論理を含む体系 BCLにPTSを与えることができると論じた。本発表では、BCLが含む「協調規則」について論じる。協調規則は、文の意味の定め方に対する要請、主張条件と否認条件が適切に関係していると言えるための条件として解釈すべきである。そのため、協調規則を設定するなら、なぜ文の意味の定め方に特定の要請が課せられるのか正当化しなければならない。BCL の協調規則のうち、無矛盾則とマイナスの帰謬法についてはこれが可能であるが、プラスの帰謬法については一定の困難がある。双側面説に加えて反証主義の立場を取ることで、プラスの帰謬法を認めることができる。（２）符号付き自然演繹を用いた否定概念の分析（五十嵐涼介）これまで多くの研究者が古典的否定、直観主義否定を始めとした様々な否定概念の差異および関係の分析を行なってきた（cf. Dunn; 1999, Shramko; 2005, Ripley 2009) 。これらの研究は主にモデル論的な観点から成されており、可能世界意味論および両立不可能性関係などの道具立てを用いて、多様な否定概念を統一的に扱っている。ところで近年、鈴木 (2015) はRumfitt(2000) において提示された符号付き自然演繹の体系を発展させ、古典論理に対して証明論的意味論の立場からより適切な正当化を与えた。本研究はこの結果を発展させ、否定概念を分析するための統一的な枠組みを与えることを目的としている。本研究は以下のような着想に基づいている。証明論的意味論の立場から様々な論理体系を統一的に扱う枠組みとしては、Dosen (1989) およびSambin et al (2000) のものがあるが、彼らはシークエント計算を用いた上で、推論規則を論理結合子の振舞いを記述する操作規則と、メタレベルの構造の関係を記述する構造規則の区別に着目した。操作規則は論理規則の定義そのもであるため、すべての体系を通じて同一である。その上で、各々の体系はどの構造規則を採用するかによって特徴付けられる。Rumfitt (2000) および鈴木 (2015) の体系も同様に、論理結合子の定義にあたる操作規則と、符号同士の関係を一般的に定めるところの協調規則を持つ。本研究では、各々の協調規則がそれぞれどのような否定概念（および論理体系）に対応するのかを明かにし、同時にそれらに対する証明論的意味論の立場からの直観的な解釈を行う。参考文献 Rummfitt, I. (2000). Yes'and `No',' Mind,109,436 781-823. (2007). `Assertingand excluding: Steps towards an anti-realist account of classical consequence,'in Auxier, R. & Hahn, L. eds. The Philosophy of Michael Dummett: Open CourtPub Co, 639-693.

1 0

応用哲学会サテライト研究会「論数哲2016」のお知らせ
by Shunsuke Yatabe 01 May '16

01 May '16

皆様、このたび、5月6日（金）に、応用哲学会第8回研究大会（2016）のサテライト研究会として、東京・お茶の水女子大学において、以下の要領で論理学と数学の哲学に関する研究会を開催することになりましたので、ご案内申し上げます。 ******************************************************************** 応用哲学会第8回研究大会（2016）サテライト研究会「論数哲2016」日時：5月6日（金）13:00-17:50 場所：お茶の水女子大学理学部３号館２Ｆ会議室（以下の地図の建物20） http://www.ocha.ac.jp/help/campusmap_l.html <http://www.ocha.ac.jp/access/campusmap_l.html> 東京都文京区大塚2-1-1 丸ノ内線茗荷谷駅徒歩7分、または有楽町線護国寺駅徒歩7分）備考：お茶の水女子大学に入構する際には、守衛所にて身分証明書の提示を求められます。＊終了後には懇親会を予定しています。【講演者・スケジュール】 1. 小山田圭一（東京工業大学） - 講演：13:00-14:00 題目：名辞・概念・対象の意味論的関係に基づく新しい論理体系について - 要旨：本発表では、名辞・概念・対象の意味論的関係を反映した内包的論理の新しい体系を提示する。提示される体系の意味論では、可能世界意味論に基づく内包的論理の体系では扱うことができない古典的な意味での内包や外延を定義することができる。また、「２は最小の素数である」のような数学的命題を必然的なものとした場合、可能世界意味論を用いた理論では、「２」の内包と「最小の素数」の内包を区別できないことになってしまうが（この取り扱いは、例えば「２は最小の素数である」を綜合命題としながらその必然性を認める立場を排除してしまう）、我々が導入する体系はその区別を可能にするものであることが示される。さらに、新しい意味論における完全性定理など、いくつかの結果についても概観される。 - 質疑応答：14:00-14:30 2. 大森仁（京都大学） - 講演：14:40-15:40 題目：Towards a unification of paraconsistent logics - 概要： Paraconsistent logics are characterized by the failure of *ex contradictione quodlibet* (ECQ hereafter). Since the modern birth of paraconsistency, infinitely many systems of paraconsistent logic have been devised and studied based on various motivations. After all, it seems that paraconsistent logics are only loosely connected to each other by a rather general requirement that ECQ should be invalid. But is it really impossible to unify paraconsistent logics? The purpose of the paper is to explore that possibility. The paper aims at the following claim: paraconsistent negations of the four-valued logic of Nuel Belnap and Michael Dunn and the three-valued logic known as the Logic of Paradox, developed by Graham Priest, are at the core of paraconsistency. Different systems of paraconsistent logic can then be classified by the additional connectives and their semantics. The first half of the paper discusses the classification. In the second half of the paper, we address the question as to whether we can include Jaskowski’s discussive logic in this picture. We show that there is an affirmative answer to this question. - 質疑応答：15:40-16:10 3. 山森真衣子（京都大学） - 講演：16:20-16:50 題名「語り得ぬもの」のパラドクス講演要旨「語り得ぬもの」という語は古今東西を問わず様々な思想で立ち現れてきた概念である。しかし広く知られているように、この概念は矛盾を惹起する。というのも、「xは語り得ぬものである」と言ったとき、xは当の「語り得ぬものである」という語によって事実語られてしまうため、「xは語り得ぬものである、かつ、語り得ぬものではない」が導かれてしまうからだ。このパラドクスを解消して「語り得ぬもの」を無矛盾に使用しようとしてきた人々もあったが、彼らの試みは失敗に終わっている。その理由として、一つには、彼らはこのパラドクスがなぜ生じるのかということに、すなわちパラドクスのメカニズムにあまり注目してこなかったことが挙げられよう。本発表は、このパラドクスのメカニズムにフォーカスを当てるものである。 - 質疑応答：16:50-17:20 4. 福田陽介（京都大学） - 講演：17:30-18:00 Title: Lambda Calculus for Classical Logic and Bilateralism in Proof-Theoretic Semantics - Abstract: The Curry-Howard isomorphism is a notion which expresses the correspondence between mathematical proofs and computer programs. It is also known as "propositions-as-types" or "proofs-as-programs": propositions corresponds to types (which are restrictions for programs as Russell used for his theory in order to overcome the Russell's paradox); proofs corresponds to programs since some kind of programming language can be seen as realizability interpretation models of constructive logic. Thanks to the isomorphism, we can clarify what notions are common, and what notions essentially belong in part of logic or part of computation. In this talk, two parts will be given. Firstly, I will introduce a well-known isomorphism, which was originally found by Griffin, between a lambda calculus (a programming language) and a classical natural deduction. Secondly, I will discuss similarities and dissimilarities between such calculi for classical logic and bilateralism in proof-theoretic semantics. - 質疑応答：18:00-18:30 オーガナイザー：五十嵐涼介、矢田部俊介

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml May 2016