Logic-ml February 2015

12 participants
17 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

CSL 2015 - call for papers
by Kazushige TERUI 01 Mar '15

01 Mar '15

みなさま Computer Sicence Logic 2015のご案内をさせていただきます。アブストラクト締切は４月３日となっております。どうぞ奮ってご投稿ください。照井 ______________________________________________________________________________________________ CSL 2015 COMPUTER SCIENCE LOGIC 2015 Berlin, 7 - 10 September 2015 http://logic.las.tu-berlin.de/csl2015/ Call for Papers _______________________________________________________________________________________________ AIM AND SCOPE Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. LOCATION The 24th EACSL Annual Conference on Computer Science Logic will be held at the Technical University Berlin from Monday, 7 September 2015 to Thurday, 10 September 2015. LIST OF TOPICS OF INTEREST (NON EXHAUSTIVE) • automated deduction and interactive theorem proving • constructive mathematics and type theory • equational logic and term rewriting • automata and games, game semantics • modal and temporal logic • model checking • decision procedures • logical aspects of computational complexity • finite model theory • computational proof theory • bounded arithmetic and propositional proof complexity • logic programming and constraints • lambda calculus and combinatory logic • domain theory • categorical logic and topological semantics • database theory • specification, extraction and transformation of programs • logical aspects of quantum computing • logical foundations of programming paradigms • verification and program analysis • linear logic • higher-order logic • nonmonotonic reasoning INVITED SPEAKERS * Martín Abadi (Santa Cruz) * Elham Kashefi (Edinburgh) * Markus Lohrey (Siegen) * Ryan Williams (Standford) IMPORTANT DATES Abstract submission: 3 April 2015 Paper Submission: 10 April 2015 Paper Notification: 13 June 2015 Conference: 7 - 10 September 2015 SUBMISSION Authors are invited to submit papers of not more than 15 pages in LIPIcs style presenting work not previously published. Papers are to be submitted through Easychair. Submitted papers must be in English and must provide sufficient detail to allow the PC to assess the merits of the paper. Full proofs may appear in a technical appendix which will be read at the reviewers' discretion. Authors are strongly encouraged to include a well written introduction which is directed at all members of the program committee. The submission is in two stages. Abstract submissions are due on 3 April 2015. Full paper submissions must be done on or before 10 April 2015. Papers must not be submitted concurrently to another conference with refereed proceedings. The PC chair should be informed of closely related work submitted to a conference or a journal. Papers authored or co-authored by members of the Programme Committee are not allowed. SATELLITE EVENTS * The 11th International Workshop on Fixed Points in Computer Science (FICS'15) will be held on 11 and 12 September 2015 as a co-located event of CSL’15. * YuriFest: we will celebrate Yuri Gurevich’s 75th birthday with a symposium in his honour on 11 and 12 September 2015 as a co-located event of CSL’15. * The annual meeting of the GI Fachgruppe Logik will be organised at the Technical University Berlin in conjunction with CSL'15. PROGRAMME COMMITTEE • Albert Atserias (Universitat Politècnica de Catalunya, Barcelona) • Achim Blumensath (Technical University Darmstadt) • Mikolaj Bojanczyk (Warsaw University) • Maria Paola Bonacina (Università degli Studi di Verona) • Patricia Bouyer-Decitre (LSV, CNRS & ENS de Cachan) • Ugo Dal Lago (Università di Bologna) • Maribel Fernández (King's College London) • Richard Garner (Macquarie University, Sydney) • Rajeev Goré (Australian National University, Canberra) • Stéphane Graham-Lengrand (CNRS & École Polytechnique, Paris-Saclay) • Martin Grohe (RWTH Aachen University) • Lauri Hella (University of Tampere) • Martin Hofmann (Ludwig-Maximilians-University Munich) • Stephan Kreutzer (Technical University Berlin, pc chair) • Martin Lange (University of Kassel) • Luigi Santocanale (LIF, Aix-Marseille Université & CNRS) • Alexandra Silva (Radboud University Nijmegen) • Alex Simpson (University of Edinburgh) • Sonja Smets (University of Amsterdam) • Makoto Tatsuta (National Institute of Informatics, Tokyo) • Kazushige Terui (Kyoto University) • James Benjamin Worrell (University of Oxford) • Nobuko Yoshida (Imperial College London) ORGANISING COMMITTEE: • Christoph Dittmann (Technical University Berlin) • Viktor Engelmann (Technical University Berlin) • Stephan Kreutzer (Technical University Berlin, Chair) • Jana Pilz (Technical University Berlin) • Roman Rabinovich (Technical University Berlin) • Sebastian Siebertz (Technical University Berlin) ------------------------------------------ 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

JAIST Logic Seminar Series
by Hajime Ishihara 28 Feb '15

28 Feb '15

皆様ストックホルム大学のErik Palmgren先生の連続講義のお知らせです。ふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 e-mail: ishihara(a)jaist.ac.jp -------------------------------------------------- * JAIST Logic Seminar Series * * This seminar is held as a part of the EU FP7 Marie Curie Actions IRSES project CORCON (http://corcon.net/). Date: Lecture 1. Monday 9 March, 2015, 15:10-16:40 Lecture 2. Tuesday 10 March, 2015, 15:10-16:40 Lecture 3. Wednesday 11 March, 2015, 15:10-16:40 Place: JAIST, Lecture room I3-I4 (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Professor Erik Palmgren (Department of Mathematics, Stockholm University) Title: Lectures on type theory with a view towards formalizing Bishop-style mathematics Abstract: In this series of three lectures we give an introduction to Martin-Lof type theory and the tools it provides for formalizing Bishop-style constructive mathematics. The first lecture will cover basic principles of type theory and give an introduction to its manifestation in the well-known proof assistant Coq. In the second lecture we consider "Bishop's set theory" (Bishop and Bridges 1985) from the point of view of type theory, which will involve a development the theory of setoids and subsetoids. The third lecture will cover models constructive set theory (CZF) in type theory, and how it can be used to solve the problem of universes of setoids and development of category theory. Throughout the lectures we provide examples and suggestions how you can yourself experiment with the Coq system in the formalization of constructive mathematics. References E. Bishop and D.S. Bridges. Constructive Analysis. Springer 1985. E. Palmgren. Lecture notes on Type Theory. Stockholm 2014. URL: http://kurser.math.su.se/course/view.php?id=48 E. Palmgren and O. Wilander. Constructing categories and setoids of setoids in type theory. Logical Methods in Computer Science. 10(2014), Issue 3, paper 25.

1 1

論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri)
by Yuta Takahashi 25 Feb '15

25 Feb '15

みなさま、こんにちは、慶応大学の高橋優太と申します。この場をお借りして、次のワークショップをお知らせさせていただきます。重複して受け取られた場合はどうかご容赦ください。 ---- 論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri) 次のような「論理哲学ワークショップ」を予定しております。今回は特に、現代論理の歴史的背景についても議論します。参加自由です。 The following Workshop on Philosophy of Logic is scheduled. The historical background of some modern logic will be discussed among others. 日時/Date&Time: 2015年2月27日(金) 14:00-17:00, Feb 27 (Fri), 2015 場所: 慶應大学三田キャンパス南館地下4階ディスタンスラーニングルーム Place: Distance Learning Room (Basement 4F), South Building, Mita campus of Keio University. ( http://www.keio.ac.jp/en/maps/mita.html 13番の建物です。/ Building #13 on this map. ) ---- 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs --------------------------------------------------------------------- 問合せ先: Mita Logic Seminar 思考と行動判断の研究拠点事務局 logic(a)abelard.flet.keio.ac.jp ABSTRACTS ENCLOSED BELOW: 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic Abstract: After the publication of his Begriffsschrift, Frege distanced himself from the Booleans by insistently opposing the content that his logic was able to express to the abstraction of Boolean logic. Frege’s commitment to the notion of content would last until the end of his work, becoming in particular the source of his famous distinction between sense and denotation. But what did Frege exactly mean by this opposition between “contentual” (inhaltlich) and abstract, as a properties of logical systems? A semiotic perspective on the constitution of Boolean logic shows that this distinction can be associated with the one between Arithmetic and Algebra, considered as different mathematical practices on signs respectively underpinning the constitution of these two logical systems. Moreover, a particular attention paid to Boole's own voluntary deviations from what would soon become the standard Boolean system permits to identify different figures of what can be seen as a content dimension arising as a logical effect of the semiotic properties of Arithmetic. 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs Abstract: Gerhald Gentzen gave three consistency proofs for number theory. These consistency proofs have a common aim that originates from Hilbert's Program. Hilbert, in his program, aimed to justify the use of ideal propositions in mathematics, by showing that no contradiction can be derived in a formal system of the ideal parts of mathematics. Gentzen aimed to justify the use of ideal propositions in number theory, and this aim is prominent especially in Gentzen's 1938 consistency proof. In Gentzen's 1935/36 consistency proofs, there is another aim that is not found in Hilbert's Program. The aim is to formulate a ``finitary'' interpretation that gives a meaning to every ideal proposition of number theory and makes the theory sound. In this talk, first we argue that what motivated Gentzen to give such an interpretation is an intuitionists' objection against the significance of consistency proofs. Second, we show that his way of the interpretation appealed to a notion being very close to the notion of spreads, which was introduced in intuitionistic mathematics. As a consequence, we claim that intuitionism was deeply related to both Gentzen's motivation and method for the interpretation. END OF ANNOUNCEMENT------------------------------------------------

1 0

KusatsuSeminar3/16--20: just a reminder
by Fujita Kenetsu 24 Feb '15

24 Feb '15

皆様，『ラムダ計算と論理の早春セミナー』のご案内　（再送）日程：2015年3月16日(月) 午後5時から3月20日(金) 正午まで場所：国立大学草津セミナーハウス　　　〒377-1711 群馬県吾妻郡草津町大字草津字白根737 詳細：http://www.cs.gunma-u.ac.jp/~fujita/2015.03LLSinKusatsu.htm 申込・質問などは藤田（群馬大学）までご連絡をお願いします．興味をお持ちのみなさまのご参加をお待ちしております． ----------- 群馬大学　藤田憲悦

1 0

論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri)
by Yuta Takahashi 24 Feb '15

24 Feb '15

みなさま、こんにちは、慶応大学の高橋優太と申します。この場をお借りして、次のワークショップのご案内をさせていただきます。重複して受け取られた場合はご容赦ください。 ---- 論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri) 次のような「論理哲学ワークショップ」を予定しております。今回は特に、現代論理の歴史的背景についても議論します。参加自由です。 The following Workshop on Philosophy of Logic is scheduled. The historical background of some modern logic will be discussed among others. 日時/Date&Time: 2015年2月27日(金) 14:00-17:00, Feb 27 (Fri), 2015 場所: 慶應大学三田キャンパス南館地下4階ディスタンスラーニングルーム Place: Distance Learning Room (B4F), South Building, Mita campus of Keio University. ---- 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs --------------------------------------------------------------------- 問合せ先: Mita Logic Seminar 思考と行動判断の研究拠点事務局 logic(a)abelard.flet.keio.ac.jp ABSTRACTS ENCLOSED BELOW: 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic Abstract: After the publication of his Begriffsschrift, Frege distanced himself from the Booleans by insistently opposing the content that his logic was able to express to the abstraction of Boolean logic. Frege’s commitment to the notion of content would last until the end of his work, becoming in particular the source of his famous distinction between sense and denotation. But what did Frege exactly mean by this opposition between “contentual” (inhaltlich) and abstract, as a properties of logical systems? A semiotic perspective on the constitution of Boolean logic shows that this distinction can be associated with the one between Arithmetic and Algebra, considered as different mathematical practices on signs respectively underpinning the constitution of these two logical systems. Moreover, a particular attention paid to Boole's own voluntary deviations from what would soon become the standard Boolean system permits to identify different figures of what can be seen as a content dimension arising as a logical effect of the semiotic properties of Arithmetic. 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs Abstract: Gerhald Gentzen gave three consistency proofs for number theory. These consistency proofs have a common aim that originates from Hilbert's Program. Hilbert, in his program, aimed to justify the use of ideal propositions in mathematics, by showing that no contradiction can be derived in a formal system of the ideal parts of mathematics. Gentzen aimed to justify the use of ideal propositions in number theory, and this aim is prominent especially in Gentzen's 1938 consistency proof. In Gentzen's 1935/36 consistency proofs, there is another aim that is not found in Hilbert's Program. The aim is to formulate a ``finitary'' interpretation that gives a meaning to every ideal proposition of number theory and makes the theory sound. In this talk, first we argue that what motivated Gentzen to give such an interpretation is an intuitionists' objection against the significance of consistency proofs. Second, we show that his way of the interpretation appealed to a notion being very close to the notion of spreads, which was introduced in intuitionistic mathematics. As a consequence, we claim that intuitionism was deeply related to both Gentzen's motivation and method for the interpretation. END OF ANNOUNCEMENT------------------------------------------------

1 0

千葉 logic seminar
by arai toshiyasu 23 Feb '15

23 Feb '15

みなさま新井@千葉大学です。千葉 logic seminar の第5回のお知らせです。どなたでも参加できますのでどうぞ気軽にいらっしゃって下さい。問合せ先新井敏康（千葉大学） tosarai(a)faculty.chiba-u.jp ------------------------------------------ 日時：3月13日(金)13:30-15:00 場所：千葉大学理学部2号館105号室アクセスは http://www.chiba-u.ac.jp/campus_map/nishichiba/index.html の地図の黄色い理学部の中で数字2が付いている建物の1階です。 Speaker: Stan Wainer (Leeds UK) Title: A miniaturized predicativity Abstract: This talk attempts to characterize those recursive functions which are "predictably terminating" according to a finitistic point of view. The basis of the work is Leivant's (1995) theory of ramified induction over N, which has elementary recursive strength. It has been redeveloped and extended in various ways by many people. Eg. Spoors & W. (2012) built a hierarchy of ramified "input-output" theories whose strengths correspond to the levels of the Grzegorczyk hierarchy. Here, a further extension of this hierarchy is developed, with one additional input level on top (level omega). The underlying logic is an autonomously generated infinitary calculus with arbitrary finitely-many stratification levels of numerical inputs and a ramified Repetition Rule. The autonomous control on allowable ordinals is based on a weak (finitistic) notion of "pointwise transfinite induction". It turns out that the ordinal of this theory is then Gamma-0; the provably computable functions are those which are resource-bounded by the slow growing hierarchy; and these are the functions elementary recursive in the Ackermann function. ------------------------------------------------------------------------------------------

1 0

鈴木右京のセミナー (名古屋大学にて)
by Jacques Garrigue 20 Feb '15

20 Feb '15

logic-mlの皆さん、名古屋大学多元数理科学研究科のJacques Garrigueです。突然ですが、以下のセミナーを開催しますので、ご案内申し上げます。講演者:　鈴木佑京（東京大学大学院広域科学科）日時:　　2月24日（火）　10:30--12:00と13:00--14:30 会場:　　名古屋大学　理学A館　A328号室タイトル:　可述算術の世界アブストラクト: エドワード・ネルソンは、古典的算術に対するオルタナティブでありながら、直観主義的算術や有限主義的算術とも異なる――より徹底した構成主義の立場に立つ ――自然数論として、「可述算術」と呼ばれる理論を提案した。彼の理論は、後の限定算術の研究に影響をあたえるとともに、数学的帰納法に関する独特な分析を含んでおり、極めて興味深い。この講演では、１）まずネルソンの構成主義的な思想を説明した後、２）可述算術の数学的展開を解説することで、まず可述算術に対するイントロダクションを行う。そののち、３）ネルソンのような改訂主義とは異なる、講演者自身の観点から、可述算術の持つ概念的な興味を解説する。ここでは、可述算術が、ウィトゲンシュタインなどが展開した「概念形成としての数学」という描像をモデル化したものであることが主張される。

1 0

鈴木右京のセミナー (名古屋大学にて)
by Jacques Garrigue 20 Feb '15

20 Feb '15

1 0

Call for Papers: Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics
by Makoto Kanazawa 18 Feb '15

18 Feb '15

Call for Papers Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics Dates: June 10-12, 2015 Location: Montpellier, France Workshop Webpage: https://sites.google.com/site/epsilon2015workshop/ Contact email: Epsilon2015(a)easychair.org Submission deadline: April 1st, 2015 Submission webpage: https://easychair.org/conferences/?conf=epsilon2015 Organizers / workshop co-chairs: Stergios Chatzikyriakidis, LIRMM-CNRS, University of Montpellier Fabio Pasquali, University of Marseille Christian Retoré, University of Montpellier & LIRMM-CNRS Host: I2M-CNRS and University of Montpellier Workshop information: This workshop aims at promoting work on Hilbert’s epsilon calculus in a number of relevant fields ranging from Philosophy and Mathematics to Linguistics and Informatics. The Epsilon and Tau operators were introduced by David Hilbert, inspired by Russell's Iota operator for definite descriptions, as binding operators that form terms from formulae. One of their main features is that substitution with Epsilon and Tau terms expresses quantification. This leads to a calculus which is a strict and conservative extension of First Order Predicate Logic. The calculus was developed for studying first order logic in view of the program of providing a rigorous foundation of mathematics via syntactic consistency proofs. The first relevant outcomes that certainly deserve a mention are the two "Epsilon Theorems" (similar to quantifiers elimination), the first correct proof of Herbrand’s theorem or the use of the Epsilon operator in Bourbaki’s Éléments de Mathématique. Nowadays the interest in the Epsilon substitution method has spread in a variety of fields: Mathematics, Logic, Philosophy, History of Mathematics, Linguistic, Type Theory, Computer science, Category Theory and others. Submission The workshop welcomes submissions of up to 4 (but not less than 2) pages. Usual spacing, font and margin should be used (single-spaced, 11pt or larger, and 1 inch margin on A4 or letter size paper). Abstracts should be submitted by April 1st, 2015 as pdf files through the EasyChair conference system ( https://easychair.org/conferences/?conf=epsilon2015). An indicative list of themes that are of particular interest to the conference are (non-exhaustive): - History of Logic - Philosophy - Proof theory - Model theory - Category theory - Type theory - Quantification in Natural language - Noun-Phrases Semantics - Proof Assistants (e.g. Coq, Isabelle, ... ) - Other subnectors (e.g. Russell's iota, μ-operator, ... ) Reviewing: Abstracts will be reviewed by members of the program committee, and, where appropriate, outside reviewers. The organizers will be responsible for making decisions partly in consultation with the program committee. Notifications will be made by May 1st, 2015. Post-Proceedings: Selected papers from the workshop will appear as a special volume in Journal of Logics and their Applications Important dates: April 1st, 2015: Submission deadline May 1st,2015: Notification of acceptance June 10-12, 2015: Workshop Invited speakers: Claus-Peter Wirth (University of Saarland): The descriptive operators iota, tau and epsilon - on their origin, partial and complete specification, model- theoretic semantics, practical applicability (with the support of the Hilbert Bernays Project (sponsored by IFCoLog)). Vito Michele Abrusci (University of Roma Tre): Hilbert's tau and epsilon in proof theory. Hartley Slater (University of Western Australia): Linguistic and philosophical ramifications of the epsilon calculus. Program Committee: Daisuke Bekki (Ochanomizu University) Stergios Chatzikyriakidis (LIRMM-CNRS & University of Montpellier) Francis Corblin (University of Paris-Sorbonne & Institut Jean Nicod CNRS) Michael Gabbay (University of Cambridge) Makoto Kanazawa (National Institute of Informatics of Tokyo) Ruth Kempson (King's College, London) Alda Mari (CNRS Institut Jean Nicod & ENS & EHESS) Georg Moser (University of Innsbruck) Bruno Woltzenlogel Paleo (Vienna University of Technology) Michel Parigot (CNRS-PPS & University of Paris Diderot 7) Fabio Pasquali (University of Aix-Marseille & I2M CNRS) Christian Retoré (University of Montpellier & LIRMM-CNRS) Mark Steedman (University of Edimburgh) Richard Zach (University of Calgary)

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml February 2015