Logic-ml March 2013

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

10 participants
15 discussions

Computability and Complexity in Analysis 2013
by Akitoshi Kawamura 12 Apr '13

12 Apr '13

皆様東京大の河村と申しますお世話になっておりますメーリングリストをお借りして七月に仏ナンシーにて開催されます解析学に於る計算可能性と計算量に関する国際会議（CCA 2013）の御案内をさせて頂きます（投稿締切4月1日）御投稿・参加を検討頂ければ幸いです -- 河村彰星東京大学大学院情報理工学系研究科コンピュータ科学専攻助教（今井研究室） 03-5841-4097 http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/index_j.html First Call for Papers http://cca-net.de/cca2013/ The Tenth International Conference on Computability and Complexity in Analysis (CCA 2013) will take place in Nancy, France, July 8-11, 2013. The CCA 2013 Program Committee cordially invites researchers in the area of computability and complexity theory to submit papers for presentation at the conference. Topics: * Computable analysis * Complexity on real numbers * Constructive analysis * Domain theory and analysis * Theory of representations * Computable numbers, subsets and functions * Randomness and computable measure theory * Models of computability on real numbers * Realizability theory and analysis * Reverse analysis * Real number algorithms * Implementation of exact real number arithmetic Submissions: Authors are invited to submit a PDF version of an extended abstract (typically 10 pages) on the following web page: https://www.easychair.org/conferences/?conf=cca2013 Dates: Submission deadline: April 1, 2013 Notification of authors: May 6, 2013 Registration deadline: May 20, 2013 Final version: May 27, 2013 Invited Speakers: * Ulrich Berger (Swansea, UK) * Takayuki Kihara (JAIST, Japan) * Cristobal Rojas (Toronto, Canada) * Daniel Roy (Cambridge, UK) * Martin Ziegler (Darmstadt, Germany) Program Committee: * Andrej Bauer (Ljubljana, Slovenia) * Arno Pauly (Cambridge, UK) * Hannes Diener (Siegen, Germany) * Cameron Freer (MIT, USA) * Laurent Bienvenu (Paris, France) * Akitoshi Kawamura (Tokyo, Japan) * Ker-I Ko (Stony Brook, USA) * Matthias Schröder (Vienna, Austria) * Robert Rettinger (Hagen, Germany) * Ning Zhong (Cincinnati, USA), chair Local Organizers * Anne-Lise Charbonnier * Hugo Férée * Emmanuel Hainry * Mathieu Hoyrup (chair) * Emmanuel Jeandel * Romain Péchoux

1 1

Control Operators and their Semantics (COS'13) - change of dates
by Fujita Kenetsu 30 Mar '13

30 Mar '13

[Please circulate. My apologies for cross posting.] 皆様， TLCA(Typed Lambda Calculi and Applications) と RTA(Rewriting Techniques and Applications) の Satellite workshop(COS'13) がEindhovenで開催されます．皆様のご参加・投稿をお待ちしております．群馬大学　藤田憲悦 ------------------------------------------------------------------------------------------------------------------------------------ This is the COS'13 cfp with some changes of dates. While keeping *the deadline of submissions on April the 6th*, we do not require previous abstract submission, and postpone to April the 15th the deadline for contributed talks only (called EXTENDED ABSTRACTS below): Submission: April, 6 2013 (*no previous abstract submission required*) Extended abstract: April, 15 2013 (*new*) Notification: April, 29 2013 (changed) Final version: May, 15 2013 (changed) Workshop: June, 24-25 2013 ============================================================================ Control Operators and their Semantics (COS'13) - Call for Papers Satellite event of RDP'13 June 24 - 25, 2013, Eindhoven, The Nederlands http://cos2013.di.unito.it/ (modified on April, 25th) ============================================================================ Modern programming languages provide sophisticated control mechanisms, commonly referred to as control operators which are widely used to realize a variety of applications. Since we cannot escape control features, it becomes a challenge to provide them with sound reasoning principles. There is a very active research on understanding, manipulating, representing, and reasoning about elaborated non-local control structures, in particular in declarative programming languages such as functional and logic languages. Ideas and results originating from this research area have impact in many other areas of computer science, like distributed and concurrent systems, proof theory, proof mining, web programming and linguistics. For instance, the study of the logical foundations of control operators renewed the study of the connections between proofs and programs via the so-called Curry-Howard correspondence, providing new methods to extract the computational content of classical proofs. The focus of the workshop is on the interplay between syntax and semantics, namely the central question of what a program means and how it does define the intended procedure. This is a crucial issue especially in the case of control operators, since they are as powerful as potentially obscure, and programs that use them are usually more error prone than purely declarative ones. The issue of a better understanding of control is also relevant for communicating across different research areas and communities. More abstract views can be achieved via several means, that include operational semantics of formal calculi, abstract machines, algebraic specifications and rewriting, type assignment systems, denotational semantics and game semantics, category theory and logic, to say the least. Relevant topics include, but are not limited to: - continuations and delimited continuations - categorical models of continuations - compositionality and modularity of control operators - denotational semantics of control, event structures and causality - operational semantics and abstract machines - type systems for control operators - game semantics of programming languages and of logical proofs - usage of control operators in proof search and proof mining - semantics of control operators in logic programming Invited speakers: - Mattew Flatt (Univeristy of Utah) - Thomas Streicher (Universitaet Darmstadt) Program Committee: Zena Ariola University of Oregon Stefano Berardi Turin University Hugo Herbelin INRIA and Laboratoire PPS (Paris 7) Ugo de'Liguoro (chair) Turin Univerisity Ken-etsu Fujita Gunma University Koji Nakazawa Kyoto University Alexis Saurin (co-chair) INRIA and Laboratoire PPS (Paris 7) Submission: authors of original works on the topic of the workshop are invited to submit either a FULL PAPER of up to 20 pages, which has to be unpublished nor submitted elsewhere, or an EXTENDED ABSTRACT of up to 5 pages (to which previous restrictions do not apply) for short presentation at the workshop. Only accepted full papers will appear in the proceedings; the PC might decide, on the ground of referees reports, that a full paper submission is accepted as extended abstract instead. Submission consists of a LaTex generated pdf file, prepared using EPTCS macro package, available from: http://info.eptcs.org/ Authors of extended abstracts must add: "Extended Abstract" to the title. The PC Submissions are via EasyChair COS2013 site: https://www.easychair.org/conferences/?conf=cos2013 Important Dates: Submission: April, 6 2013 (no previous abstract submission required) Extended abstract: April, 15 2013 (new) Notification: April, 29 2013 (changed) Final version: May, 15 2013 (changed) Workshop: June, 24-25 2013 Contact: Ugo de'Liguoro Dipartimento di Informatica, Universita' di Torino, Corso Svizzera 185, 10149 Torino, Italy email: deliguoro(a)di.unito.it <mailto:deliguoro@di.unito.it> Web sites: COS'13: http://cos2013.di.unito.it <http://cos2013.di.unito.it/> RTD'13: http://www.win.tue.nl/rdp2013/ ------------------------------------------------------------------------------------------------

1 0

Computability in Europe 2013
by Akitoshi Kawamura 28 Mar '13

28 Mar '13

皆様東京大の河村と申しますお世話になっておりますメーリングリストをお借りして七月に伊ミラノで開催されます欧洲計算可能性会議CiE 2013の御案内をさせていただきます投稿締切が二週間後に迫っておりますが御投稿・御参加を検討頂ければ幸いです -- 河村彰星東京大学大学院情報理工学系研究科コンピュータ科学専攻助教（今井研究室） 03-5841-4097 http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/index_j.html ************************************************************************ CiE13 CALL FOR PAPERS AND SPECIAL AWARDS: CiE 2013: The Nature of Computation: Logic, Algorithms, Applications Milan, Italy July 1 - 5, 2013 http://cie2013.disco.unimib.it IMPORTANT DATES: Submission Deadline for LNCS: 20 January 2013 Notification of authors: 4 March 2013 Deadline for final revisions: 1 April 2013 CiE 2013 is the ninth conference organised by CiE (Computability in Europe), a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world. Previous meetings have taken place in Amsterdam (2005), Swansea (2006), Siena (2007), Athens (2008), Heidelberg (2009), Ponte Dalgada (2010), Sofia (2011) and Cambridge (2012). The Nature of Computation is meant to emphasize the special focus of CIE13 on the unexpected and strong changes that studies on Nature have brought in several areas of mathematics, biology, physics, and computer science. Starting from Alan Turing, research on Nature with a computational perspective has produced novel contributions, giving rise even to new disciplines. AWARDS: Springer-Verlag has graciously funded two awards that will be given during the CiE 2013 Conference. Best student paper: This prize will be awarded for the best student paper presented at CiE 2013, as judged by the Program Committee. A prize of 500 euros will be given to the author(s) of the best student-authored paper (or split between more than one paper if there is a tie). In order to be considered, a paper has to be submitted in the category 'Regular paper (eligible for best student paper award)' on EasyChair. Papers are eligible if all of its authors are full-time students at the time of submission. Best paper on Natural Computing: The prize consists of the four volumes of the Handbook of Natural Computing (see http://cie2013.disco.unimib.it/awards/). This prize will be awarded to the best paper on Natural Computing presented at CiE 2013, as judged by the Program Committee. A paper is eligible if its main topic falls within the scope of Natural Computing, roughly defined as the set of fields studied in the above handbook. The Program Committee is the only judge of the relevance of a paper within the Natural Computing scope. The authors of a paper eligible for the award must indicate this in the submission notes. INVITED SPEAKERS Ulle Endriss (University of Amsterdam) Lance Fortnow (Georgia Institute of Technology) Anna Karlin (University of Washington) Bernard Moret (Ecole Polytechnique Federale de Lausanne) Mariya Soskova (Sofia University) Endre Szemeredi (Hungarian Academy of Sciences, Rutgers University) TUTORIAL SPEAKERS Gilles Brassard (Universite de Montreal) Grzegorz Rozenberg (Leiden Institute of Advanced Computer Science and University of Colorado at Boulder) SPECIAL SESSIONS on Algorithmic Randomness organizers: Mathieu Hoyrup, Andre Nies Data Streams and Compression organizers: Paolo Ferragina, Andrew McGregor Computational Complexity in the Continuous World organizers: Akitoshi Kawamura, Robert Rettinger Computational Molecular Biology organizers: Alessandra Carbone, Jens Stoye Computation in Nature organizers: Mark Delay, Natasha Jonoska History of Computation organizers: Gerard Alberts, Liesbeth De Mol PROGRAM COMMITTEE: * Gerard Alberts (Amsterdam) * Luis Antunes (Porto) * Arnold Beckmann (Swansea) * Laurent Bienvenu (Paris) * Paola Bonizzoni (Milan, co-chair) * Vasco Brattka (Munich and Cape Town, co-chair) * Cameron Buckner (Houston TX) * Bruno Codenotti (Pisa) * Stephen Cook (Toronto ON) * S Barry Cooper (Leeds) * Ann Copestake (Cambridge) * Erzsebet Csuhaj-Varju (Budapest) * Anuj Dawar (Cambridge) * Gianluca Della Vedova (Milan) * Liesbeth De Mol (Gent) * Jerome Durand-Lose (Orleans) * Viv Kendon (Leeds) * Bjoern Kjos-Hanssen (Honolulu, HI) * Antonina Kolokolova (St. John's NF) * Benedikt Loewe (Amsterdam) * Giancarlo Mauri (Milan) * Rolf Niedermeier (Berlin) * Geoffrey Pullum (Edinburgh) * Nicole Schweikardt (Frankfurt) * Sonja Smets (Amsterdam) * Susan Stepney (York) * S. P. Suresh (Chennai) * Peter van Emde Boas (Amsterdam) The PROGRAMME COMMITTEE cordially invites all researchers (European and non-European) in computability related areas to submit their papers (in PDF format, max 10 pages using the LNCS style) for presentation at CiE 2013. The submission site https://www.easychair.org/conferences/?conf=cie2013 is open. We particularly invite papers that build bridges between different parts of the research community. The CONFERENCE PROCEEDINGS will be published by LNCS, Springer Verlag. Contact: Paola Bonizzoni - bonizzoni at disco.unimib.it Website: http://cie2013.disco.unimib.it

1 2

講演会/セミナーのお知らせ
by Makoto Kikuchi 24 Mar '13

24 Mar '13

各位先日ご案内しました Segei Artemov 教授， Elena Nogina 教授の講演会の場所が間違えていたので訂正します．日本大学文理学部1号館1階122教室とあったのは誤りで，正しくは日本大学文理学部1号館2階122教室です．よろしくお願いします．菊池誠 -- 各位先日ご案内いたしました Segei Artemov 教授 (City University of New York)，Elena Nogina 教授 (City University of New York) の講演会とセミナーのアブストラクトをお送りします．（一部，講演題目が変更されています．）講演会，セミナーにご出席希望の方は事前にそれぞれの問い合わせ先までご連絡下さい．【１】論理学講演会日時：2013年3月24日（日）14:30-18:00 場所：日本大学文理学部1号館1階122教室プログラム: 14:30-16:00 Sergei Artemov (CUNY) Formalizing Brouwer-Heyting-Kolmogorov semantics 16:30-18:00 Elena Nogina (CUNY) Joining Two Goedel's Models of Provability アブストラクト： Speaker: Sergei Artemov, The City University of New York Title: Formalizing Brouwer-Heyting-Kolmogorov semantics Abstract: According to Brouwer, intuitionistic truth is provability; this led to the informal Brouwer-Heyting-Kolmogorov (BHK) semantics of proofs for intuitionistic logic (1934). There are two well-known problems with BHK exposed by Kreisel in 1962. First, in the original BHK, any proof vacuously “proves” the negation of any unprovable sentence; this dubious feature ruins constructive connection between a sentence and its proof. Second, original BHK’s treating of universal quantifiers admits unacceptable bogus “proofs” for any true Π1-sentence, e.g., for Fermat’s Last Theorem or the consistency statement. Kreisel offered plausible corrections to BHK which we suggest calling BHK*. The problem of an exact provability interpretation of BHK* turned out to be elusive. For example, BHK- inspired semantics based on computational programs (Realizability, Curry-Howard isomorphism, Intuitionistic Type Theory) though have constituted a major development in logic and computer science, do not satisfy BHK*. In the 1930s, Gödel suggested to define intuitionistic logic via classical provability represented by modal logic S4 and interpret the latter via explicit proofs rather then provability. Later developments of the Logic of Proofs LP in the 1990s opened the door to realizing Gödel’s approach. In this talk, we survey provability semantics obtained by Gödel’s embedding of intuitionistic logic into S4, followed by a realization in the Logic of Proofs. We show that it satisfies BHK* requirements and provides a desired provability foundation for intuitionistic logic. Speaker: Dr. Elena Nogina, The City University of New York Title: Joining Two Gödel's approaches to provability Abstract: In 1933, Gödel suggested S4 as a modal logic of provability but pointed out that S4 was not compatible with a straightforward interpretation of modality as formal provability. This left "a provability semantics without a calculus" and "a provability calculus without a semantics." In 1976, Solovay found that modal logic GL was the logic of formal provability; in 1995, Artemov found a precise provability semantics for S4 via Logic of Proofs LP. In this talk, we introduce logic GLA representing both aforementioned Gödel's approaches to provability, as well as new provability principles which appear as a result of interactions between these models. GLA is supplied with a Kripke-style semantics and the corresponding completeness theorem. Soundness and completeness of GLA with respect to the arithmetical provability semantics is established. 問い合わせ先：日本大学文理学部哲学科飯田隆 iida.takashi19(a)nihon-u.ac.jp 【２】Seminar in Logic and Philosophy of Mathematics 日時：2013年3月26日（火）〜27日（水）場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）プログラム： 3月26日 10:30-12:00 Sergei Artemov (CUNY) Logic of Proofs and Justification (1/2) 13:00-14:30 Elena Nogina (CUNY) On Provability and Explicit Proofs 15:00-16:30 Taishi Kurahashi (Kobe) Syntax and semantics of predicate modal logic of provability 3月27日 10:30-12:00 Sergei Artemov (CUNY) Logic of Proofs and Justification (2/2) 13:00-14:30 Ryota Akiyoshi (Kyoto) Proper Explanation of Brouwer's Fundamental Assumption 15:00-16:30 Hidenori Kurokawa Kreisel's second clause and the theory of constructions Speaker: Sergei Artemov, The City University of New York Title: Logic of Proofs and Justification Abstract: We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t:F that read `t is a justification for F.' In this talk, we show how Justification Logic originated from the mathematical proof-theoretical semantics as the Logic of Proofs and then extended to the mainstream epistemology. In the foundations of constructive reasoning, the Logic of Proofs has completed Gödel's effort of the 1930s to find a classical provability interpretation of intuitionistic logic. In epistemology, Justification Logic offered the missing justification component to formal analysis of Knowledge as Justified True Belief approach commonly attributed to Plato. As a case study, we offer a resolution of the Goldman–Kripke ‘Red Barn’ paradox and analyze Russell’s ‘prime minister example’ in Justification Logic. We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a robust system of justifications. This renders a new, evidence-based foundation for epistemic logic. Speaker: Dr. Elena Nogina, The City University of New York. Title: On Provability and Explicit Proofs Abstract: Gödel's Incompleteness Theorem drew a sharp distinction between explicit proofs and formal provability. In particular, reflection principle "if A is formally provable then A holds" is true but not internally provable, whereas explicit reflection principle "if p is a proof of A, then A holds" is both true and provable. According to Solovay, all valid principles of formal provability are described by Gödel-Löb modal logic GL. Artemov's Logic of Proofs LP describes all valid principles of explicit proofs with a basic set of operations. Some meaningful provability principles require both provability and explicit proofs. E.g., the negative introspection fails in GL as well as in LP, but admits an adequate formulation in mixed language of GL and LP. We introduce logic GLA, that describes, along with GL and LP, all valid principles in the language of proofs and provability. GLA has been supplied with Kripke-style semantics and shown to be complete with respect to the intended arithmetical provability interpretation. 問い合わせ先：神戸大学大学院システム情報学研究科菊池誠 mkikuchi(a)kobe-u.ac.jp

1 0

ランダムネスの研究集会講演募集
by Kenshi Miyabe 23 Mar '13

23 Mar '13

皆様宮部です．ランダムネスの研究集会のお知らせです． ---- ランダムネスに関する研究集会を次のように開催します．集会名：ELC Workshop on Randomness and Probability Through Computability (RPTC2013) 日時：2013年5月14日(火)15日(水) 場所：東京大学本郷キャンパス内 http://kenshi.miyabe.name/rptc2013/ 直前の2013年5月13日(月)14日(火)には，同じ場所でランダムネスのセミナーも行う予定です． ELC Seminar on Algorithmic Randomness http://kenshi.miyabe.name/rptc2013/seminar.html 本研究集会には，ランダムネスの理論を主導している二人である Prof. DowneyとProf. Niesに参加・講演して頂きます．また他の招待講演者として Prof. Bakhadyr Khoussainovと九州大学の来嶋秀治准教授 http://tcslab.csce.kyushu-u.ac.jp/~kijima/index_j.html を招待いたしました．つきましては，国内より講演を募集します．ランダムネスもしくはランダムネスに関連する分野の研究や紹介，提案などで，招待講演者らに聞いてもらいたいという内容を歓迎します．名前，所属，講演タイトル，１パラグラフ程度の要旨，旅費を希望するかどうかを添えて，宮部 kmiyabe(a)kurims.kyoto-u.ac.jp までメールでお申し込み下さい．採択・不採択の通知後，アブストラクトをTeXで投稿していだきます．アブストラクトの長さは自由ですが，A4で1ページ以下を想定しています．投稿期限：4月19日(金) 採択・不採択の通知：4月23日(火) アブストラクトの投稿期限：4月30日(火) なお，本集会は文部科学省科学研究費補助金新学術領域研究「多面的アプローチの統合による計算限界の解明」 http://www.al.ics.saitama-u.ac.jp/elc/ の支援を受けております．東京大学情報理工学系研究科河村彰星 kawamura(a)is.s.u-tokyo.ac.jp 京都大学数理解析研究所宮部賢志 kmiyabe(a)kurims.kyoto-u.ac.jp -- 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

講演会/セミナーのお知らせ
by Makoto Kikuchi 23 Mar '13

23 Mar '13

各位先日ご案内いたしました Segei Artemov 教授 (City University of New York)，Elena Nogina 教授 (City University of New York) の講演会とセミナーのアブストラクトをお送りします．（一部，講演題目が変更されています．）講演会，セミナーにご出席希望の方は事前にそれぞれの問い合わせ先までご連絡下さい．【１】論理学講演会日時：2013年3月24日（日）14:30-18:00 場所：日本大学文理学部1号館1階122教室プログラム: 14:30-16:00 Sergei Artemov (CUNY) Formalizing Brouwer-Heyting-Kolmogorov semantics 16:30-18:00 Elena Nogina (CUNY) Joining Two Goedel's Models of Provability アブストラクト： Speaker: Sergei Artemov, The City University of New York Title: Formalizing Brouwer-Heyting-Kolmogorov semantics Abstract: According to Brouwer, intuitionistic truth is provability; this led to the informal Brouwer-Heyting-Kolmogorov (BHK) semantics of proofs for intuitionistic logic (1934). There are two well-known problems with BHK exposed by Kreisel in 1962. First, in the original BHK, any proof vacuously “proves” the negation of any unprovable sentence; this dubious feature ruins constructive connection between a sentence and its proof. Second, original BHK’s treating of universal quantifiers admits unacceptable bogus “proofs” for any true Π1-sentence, e.g., for Fermat’s Last Theorem or the consistency statement. Kreisel offered plausible corrections to BHK which we suggest calling BHK*. The problem of an exact provability interpretation of BHK* turned out to be elusive. For example, BHK- inspired semantics based on computational programs (Realizability, Curry-Howard isomorphism, Intuitionistic Type Theory) though have constituted a major development in logic and computer science, do not satisfy BHK*. In the 1930s, Gödel suggested to define intuitionistic logic via classical provability represented by modal logic S4 and interpret the latter via explicit proofs rather then provability. Later developments of the Logic of Proofs LP in the 1990s opened the door to realizing Gödel’s approach. In this talk, we survey provability semantics obtained by Gödel’s embedding of intuitionistic logic into S4, followed by a realization in the Logic of Proofs. We show that it satisfies BHK* requirements and provides a desired provability foundation for intuitionistic logic. Speaker: Dr. Elena Nogina, The City University of New York Title: Joining Two Gödel's approaches to provability Abstract: In 1933, Gödel suggested S4 as a modal logic of provability but pointed out that S4 was not compatible with a straightforward interpretation of modality as formal provability. This left "a provability semantics without a calculus" and "a provability calculus without a semantics." In 1976, Solovay found that modal logic GL was the logic of formal provability; in 1995, Artemov found a precise provability semantics for S4 via Logic of Proofs LP. In this talk, we introduce logic GLA representing both aforementioned Gödel's approaches to provability, as well as new provability principles which appear as a result of interactions between these models. GLA is supplied with a Kripke-style semantics and the corresponding completeness theorem. Soundness and completeness of GLA with respect to the arithmetical provability semantics is established. 問い合わせ先：日本大学文理学部哲学科飯田隆 iida.takashi19(a)nihon-u.ac.jp 【２】Seminar in Logic and Philosophy of Mathematics 日時：2013年3月26日（火）〜27日（水）場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）プログラム： 3月26日 10:30-12:00 Sergei Artemov (CUNY) Logic of Proofs and Justification (1/2) 13:00-14:30 Elena Nogina (CUNY) On Provability and Explicit Proofs 15:00-16:30 Taishi Kurahashi (Kobe) Syntax and semantics of predicate modal logic of provability 3月27日 10:30-12:00 Sergei Artemov (CUNY) Logic of Proofs and Justification (2/2) 13:00-14:30 Ryota Akiyoshi (Kyoto) Proper Explanation of Brouwer's Fundamental Assumption 15:00-16:30 Hidenori Kurokawa Kreisel's second clause and the theory of constructions Speaker: Sergei Artemov, The City University of New York Title: Logic of Proofs and Justification Abstract: We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t:F that read `t is a justification for F.' In this talk, we show how Justification Logic originated from the mathematical proof-theoretical semantics as the Logic of Proofs and then extended to the mainstream epistemology. In the foundations of constructive reasoning, the Logic of Proofs has completed Gödel's effort of the 1930s to find a classical provability interpretation of intuitionistic logic. In epistemology, Justification Logic offered the missing justification component to formal analysis of Knowledge as Justified True Belief approach commonly attributed to Plato. As a case study, we offer a resolution of the Goldman–Kripke ‘Red Barn’ paradox and analyze Russell’s ‘prime minister example’ in Justification Logic. We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a robust system of justifications. This renders a new, evidence-based foundation for epistemic logic. Speaker: Dr. Elena Nogina, The City University of New York. Title: On Provability and Explicit Proofs Abstract: Gödel's Incompleteness Theorem drew a sharp distinction between explicit proofs and formal provability. In particular, reflection principle "if A is formally provable then A holds" is true but not internally provable, whereas explicit reflection principle "if p is a proof of A, then A holds" is both true and provable. According to Solovay, all valid principles of formal provability are described by Gödel-Löb modal logic GL. Artemov's Logic of Proofs LP describes all valid principles of explicit proofs with a basic set of operations. Some meaningful provability principles require both provability and explicit proofs. E.g., the negative introspection fails in GL as well as in LP, but admits an adequate formulation in mixed language of GL and LP. We introduce logic GLA, that describes, along with GL and LP, all valid principles in the language of proofs and provability. GLA has been supplied with Kripke-style semantics and shown to be complete with respect to the intended arithmetical provability interpretation. 問い合わせ先：神戸大学大学院システム情報学研究科菊池誠 mkikuchi(a)kobe-u.ac.jp

1 1

ICE 2013: Deadline extended until Sunday 24th March
by Ichiro Hasuo 20 Mar '13

20 Mar '13

みなさま，以前お知らせしたワークショップ ICE のご案内です． - 〆切が 3/24 まで延びました． - Short paper や既発表論文の紹介も大歓迎です．みなさま，ぜひご投稿・ご参加を検討ください！蓮尾一郎 http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ====== [- Apologies for multiple copies -] ICE 2013 6th Interaction and Concurrency Experience June 6, 2013, Florence, Italy http://www.discotec.org/workshops/ice2013/ Satellite workshop of DisCoTec 2013 http://www.discotec.org === Highlights === - Innovative selection procedure - ICE welcomes submissions of full papers, short papers, and brief announcements - Invited talks: Davide Sangiorgi & Damien Pous - Special issue of Science of Computer Programming (http://www.journals.elsevier.com/science-of-computer-programming/) === Important Dates === 24 March 2013...................Full paper submission 25 March - 21 April 2013....Reviews, rebuttal, and PC discussion 24 April 2013......................Notification to authors 6 June 2013.......................ICE in Florence 15 Sept 2013.....................Camera-ready for post-proceedings === Scope === Interaction and Concurrency Experiences (ICEs) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools and programming primitives for complex interactions. The general scope of the venue includes theoretical and applied aspects of interactions and the synchronization mechanisms used among components of concurrent/distributed systems, related to several areas of computer science in the broad spectrum ranging from formal specification and analysis to studies inspired by emerging computational models. Topics of interest include, but are not limited to: - Process algebra and coordination: transformation, analysis and implementation - Models for distributed coordination and semantics - Techniques and tools for specification, analysis, verification of resilient interactions - Coinductive techniques for reactive systems - Languages, protocols and mechanisms for sound distributed coordination - Logics and types for interactions - Comparison among different coordination and/or execution models - Expressive power of coordination languages and execution models - Formal semantics of coordination languages - Formal verification of distributed coordinated architectures - Relations between different semantic models for coordination languages === Selection Procedure === Since its 1st edition in 2008, the distinguishing feature of ICE has been an innovative paper selection mechanism based on an interactive discussion amongst authors and PC members. During the review phase, each submitted paper is published on a Wiki and associated with a discussion forum. The discussion forum can be accessed by the authors of the paper and by all the PC members not in conflict with the paper. The forum is used by reviewers to ask questions and clarifications to the authors, allowing them to better explain all the aspects of their paper. The evaluation of the paper will keep into account not only the reviews, but also the outcome of the discussion. As witnessed by the past five editions of ICE, this procedure considerably improves the accuracy of the feedback from reviews, the fairness of the selection, the quality of camera-ready papers, and the discussion during the workshop. === The Public Wiki === After the notification, the accepted papers are published on a public forum, in order to initiate public discussions that will trigger and stimulate the scientific debate at the workshop. We believe that this will drive the workshop discussions and let prospective participants interact with each other much earlier than in more traditional events. === Submission Guidelines === We invite for three types of submissions: (1) Full Papers, (2) Short Papers, and (3) Brief Announcements of already Published Papers. Full and short papers to appear in the post-proceedings must report previously unpublished work and not be simultaneously submitted to other conferences/workshops with refereed proceedings. The ICE 2013 post-proceedings will be published in Electronic Proceedings in Theoretical Computer Science (http://eptcs.org/). In addition, we invite for brief announcements of already published results, should the authors be interested in discussing their published research with the ICE community and giving a talk. Brief announcements will not be part of the post-proceedings. Submissions must be made electronically in PDF format via EasyChair (http://www.easychair.org/conferences/?conf=ice2013). Full papers should not exceed 15 pages while short papers and brief announcements should not exceed 5 pages with the EPTCS style (http://style.eptcs.org/). Accepted (full and short) papers and brief announcements must be presented at the workshop by one of the authors. === Special Issue === Extended versions of the best full papers selected by the PC will be invited to appear in a special issue of the journal of Science of Computer Programming (http://www.journals.elsevier.com/science-of-computer-programming/ ). Such contributions will be regularly peer-reviewed according to the standard journal policy, but they will be handled in a shorter time than regular submissions. === Program Committee === Luca Aceto (Reykjavik University, Iceland) Simon Bliudze (EPFL, Switzerland) Laura Bocchi (University of Leicester, UK) Filippo Bonchi (CNRS, France) Roberto Bruni (University of Pisa, Italy) Marcello Bonsangue (Leiden University, The Netherlands) Ornela Dardha (University of Bologna/INRIA, Italy) Ichiro Hasuo (University of Tokyo, Japan) Tobias Heindel (CEA Saclay, France) Ludovic Henrio (CNRS, France) Clemens Kupke (University of Strathclyde, Scotland, UK) Julien Lange (University of Leicester, UK) Antonia Lopes (University of Lisbon, Portugal) Giuliano Losa (EPFL, Switzerland) Claudio A. Mezzina (FBK Trento, Italy) Matteo Mio (École Polytechnique, France) Valentina Monreale (University of Pisa, Italy) Luca Mottola (Politecnico di Milano, Italy) Daniela Petrisan (University of Leicester, UK) Paola Spoletini (University of Insubria, Italy) Emilio Tuosto (University of Leicester, UK) Valerio Senni (IMT Lucca, Italy) Alexandra Silva (Radboud University Nijmegen, The Netherlands) Josef Widder (TU Vienna, Austria) Roberto Zunino (Università degli Studi di Trento and COSBI, Italy) === ICEcreamers === - Marco Carbone (IT University of Copenhagen, Denmark; co-chair) - Ivan Lanese (University of Bologna/INRIA, Italy) - Alberto Lluch Lafuente (IMT Lucca, Italy) - Ana Sokolova (University of Salzburg, Austria; co-chair) === Contact === ice2013(a)easychair.org === Previous editions === The previous five editions of ICE have been held on * July 6th, 2008 in Reykjavik, Iceland, co-located with ICALP'08. The post-proceedings were published in ENTCS (vol.229-3). * August 31st, 2009 in Bologna, Italy, co-located with CONCUR'09. The post-proceedings were published in EPTCS (vol.12) and selected papers appeared in a joint special issue of MSCS (with EXPRESS’09 and SOS’09, Vol. 22, Number 2). * June 10th, 2010 in Amsterdam, The Netherlands, co-located with DisCoTec'10. The post-proceedings were published in EPTCS (vol.38) and selected papers appeared in a joint special issue of SACS (with CAMPUS'10 and CS2BIO'10, Vol. XXI). * June 9th, 2011 in Reykjavik, Iceland, co-located with DisCoTec'11. The post-proceedings were published in EPTCS (vol.59) and selected papers appeared in a special issue of SACS (Vol. XXII). * June 16th, 2012 in Stockholm, Sweden, co-located with DisCoTec'12. The post-proceedings were published in EPTCS (vol.104) and a special issue of SCP is now in preparation.

1 0

PROBABILITY AND VAGUENESS, University of Tokyo, March 20-22, 2013
by Richard Dietz 16 Mar '13

16 Mar '13

PROBABILITY AND VAGUENESS, University of Tokyo, March 20-22, 2013 It is my pleasure to announce the upcoming Probability and Vagueness conference, which will be hosted by the Department of Philosophy at the University of Tokyo, and take place on March 20-22, 2013. For further details, please see: http://probvag-tokyo.com *Invited speakers* Eleonora Cresto (University of Buenos Aires) Igor Douven (University of Groningen) Alan Hajek (ANU) Rosanna Keefe (University of Sheffield) Dan Lassiter (University of Stanford) Aidan Lyon (University of Maryland) Peter Pagin (Stockholm University) Wlodek Rabinowicz (Lund University) Nick J.J. Smith (University of Sydney) The conference will be registration free. Please feel free to join in if you happen to be in Tokyo in the next week! Richard Dietz and Masaki Ichinose (the organisers)

1 0

Call for Workshop Proposals:JSAI-IsAI 2013
by Ken Satoh 13 Mar '13

13 Mar '13

Call for Workshop Proposals JSAI International Symposia on AI (JSAI-isAI 2013) Sponsored by: The Japanese Society for Artificial Intelligence (JSAI) Date: October 27 - 28, 2013 Venue: Raiousha Building, Keio University, Kanagawa Submission deadline: March 23, 2013 Submit a proposal to "JSAI-isAI [at] ai-gakkai.or.jp" by e-mail The fifth JSAI International Symposia on AI (JSAI-isAI) will take place at Keio University, Kanagawa on October 27th and 28th, 2013. JSAI-isAI is an event that hosts several international workshops at the same location. This is in succession to the international workshops co-located with JSAI annual conferences since 2001. JSAI invites proposals for the fifth JSAI-isAI. JSAI-isAI brings together a set of workshops at a common site, providing a unique and intimate forum for colleagues in a given discipline. JSAI-isAI also provides an important opportunity for AI researchers to get together and share their knowledge. Selected papers of JSAI-isAI workshops has been published in LNAI series as LNAI6284(isAI2009), LNAI6797(IsAI2010), LNAI7258(IsAI2011), respectively, and a volume for IsAI2012 is under editing. We expect the same treatment this year as well (under negotiation with Springer Verlag). Prospective workshop organizers should send a proposal (maximum three pages) with the following sections to the JSAI-isAI 2013 Committee. - Title of the workshop - Objectives, and scope - Names and contacts of key organizers and a tentative list of the program committee members. - Expected number of papers, attendees, and preliminary workshop format. Proposals will be reviewed by the JSAI-isAI 2013 Committee. The form for workshop proposals is shown below. ------------------------------------------------------------ <Workshop Proposal Form> Workshop title: Abstract (within 400 words): #Describe objective, scope Expected number of papers: Expected number of attendees: Preliminary workshop format: #Describe whether the workshop will include panels, posters, and etc. Past experiences in JSAI-isAI (if any): #Describe whether you have organized workshops in JSAI-isAI and how #many participants you have got in the past Information of Workshop leader (1) Name: Affiliation: Postal address: Telephone: Fax e-mail: Experiences with conference/workshop (if any): Information of Workshop co-leader (2) (if any) Name: Affiliation: Postal address: Telephone: Fax e-mail: Experiences with conference/workshop (if any): The tentative list of members in the program committee (3): ------------------------------------------------------------ Important Dates Workshop Proposal Due: 23 March 2013 Workshop Notification: 9 April 2013 Release of Workshop Call for Paper: April 2013 Workshop Submission Deadline: August 2013 Workshop Author Notification: September 2013 Workshop Camera-ready: September 2013 Workshop Date: 27-28, October 2013 (Sunday, Monday) Notes The organizers and chairs of the workshop shall have full control on the call for papers, forming of program committees, review and selection of papers as well as planning the workshop program. Furthermore, the organizers and chairs of the workshop should specify in the web page that the workshop is `with a support of The Japanese Society for Artificial Intelligence' and `in association with forth JSAI International Symposia on AI (JSAI-isAI 2013).' The organizers and chairs of the workshop are also responsible for preparing a short review of the workshop, to be printed in the journal of JSAI.

1 0

TACL2013
by 小野寛晰 13 Mar '13

13 Mar '13

TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2013) Conference and Summer School (Abstract Submission Deadline: April 1, 2013) (Support Request Deadline: April 21, 2013) ====================================================== The Sixth International Conference (and Summer School) on Topology, Algebra and Categories in conjunction with the 28th Annual Shanks Lecture Series Conference and Shanks Lectures: July 28 - August 1, 2013 Summer School: July 24 - 27, 2013 Department of Mathematics, Vanderbilt University Nashville, Tennessee USA http://www.math.vanderbilt.edu/~tacl2013/

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml March 2013