Logic-ml

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

7 participants
1772 discussions

Continuity, Computability, Constructivity 2017; second call for submission; extended deadline
by Hajime Ishihara 12 Apr '17

12 Apr '17

*Continuity, Computability, Constructivity – From Logic to Algorithms* * (CCC 2017)* * Loria, 26-30 June 2017* *Call for papers* http://ccc2017.loria.fr/ CCC is a workshop series bringing together researchers from exact real number computation, computable analysis, effective descriptive set theory, constructive analysis, and related areas. The overall aim is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and provably correctalgorithms for computations with real numbers and related analytical data, which are of increasing importance in safety critical applications and scientific computation. Previous workshops have been held in Cologne 2009, Trier 2012, Gregynog 2013, Ljubljana 2014, and Kochel 2015. The conference series has always been linked with EU-funded international research projects, with COMPUTAL (Computable Analysis) in the years 2012-2015 and now with CID (Computing with Infinite Data), a research network between Europe, Chile, Japan, New Zealand, Russia, Singapore, South Africa, South Korea, and the USA. This conference is the first CID event, but is open to all researchers in the area. The workshop will take place in Nancy, France. *Scope: *The workshop specifically invites contributions in the areas of * Exact real number computation, * Correctness of algorithms on infinite data, * Computable analysis, * Complexity of real numbers, real-valued functions, etc. * Effective descriptive set theory * Scott's domain theory, * Constructive analysis, * Category-theoretic approaches to computation on infinite data, * Weihrauch degrees, * And related areas. *Invited Speakers:* * Matthew de Brecht (Kyoto, Japan) * Bernhard Reus (Brighton, UK) * Matthias Schröder (Darmstadt, Germany) * Alex Simpson (Ljubljana, Slovenia) * * *Submission:* * * Extended abstracts (1-2 pages) of original work are welcome. * * ** *Extended Deadline:* *10 May 2017* ** *Upload your submission via EasyChair:* https://easychair.org/conferences/?conf=ccc20170 *Programme Committee:* * Ulrich Berger (Swansea) * Pieter Collins (Maastricht) * Mathieu Hoyrup (Nancy) (co-chair) * Erik Palmgren (Stockholm) * Victor Selivanov (Novosibirsk) * Dieter Spreen (Siegen) (co-chair) * Martin Ziegler (Daejeon). *Organizing Committee:* * Anne-Lise Charbonnier (Nancy) * Mathieu Hoyrup (Nancy)

2 1

FW: 松山 TGSAセミナーのお知らせ（４月１９日）
by FUJITA Hiroshi 11 Apr '17

11 Apr '17

こんにちは。愛媛大学の藤田です。次回のTGSAセミナーの案内を転送します。藤田博司 <fujita.hiroshi.mh(a)ehime-u.ac.jp> ________________________________ 差出人: Dmitri SHAKHMATOV <dmitri.shakhmatov(a)dmitri.math.sci.ehime-u.ac.jp> 送信日時: 2017年4月11日 10:55 宛先: FUJITA Hiroshi CC: dmitri.shakhmatov(a)dmitri.math.sci.ehime-u.ac.jp 件名: 松山 TGSAセミナーのお知らせ（４月１９日）皆様、「Matsuyama Seminar on Topology, Geometry, Set Theory and their Applications」（松山TGSAセミナー）のお知らせです。 ***** 第30回のセミナー日時: 2017年4月19日（水） 16:30〜17:30 場所: 愛媛大学理学部2号館2階，大演習室 (201号室) 講演者: Alejandro Dorantes-Aldama (愛媛大学) 題目: Selective sequential pseudcompactness 概要： We say that a topological space $X$ is {\em selectively sequentially pseudcompact} if for every family $\{U_n:n\in\mathbb{N}\}$ of non-empty open subsets of $X$, one can choose a point $x_n\in U_n$ for each $n\in\mathbb{N}$ in such a way that the sequence $\{x_n:n\in \mathbb{N}\}$ has a convergent subsequence. We show that the class of selectively sequentially pseudcompact spaces is closed under arbitrary products and continuous images, contains the class of all dyadic spaces and forms a proper subclass of the class of strongly pseudocompact spaces introduced recently by Garc\'ia-Ferreira and Ortiz-Castillo. We prove, under the Singular Cardinal Hypothesis SCH, that if $G$ is an Abelian group admitting a pseudocompact group topology, then it can also be equipped with a selectively sequentially pseudcompact group topology. Since selectively sequentially pseudcompact spaces are strongly pseudocompact, this provides a strong positive answer to a question of Garc\'ia-Ferreira and Tomita. This is a joint work with Dmitri Shakhmatov. 講演終了後に交流会を予定しています。交流会にご参加いただける方はシャクマトフ<dmitri.shakhmatov(a)ehime-u.ac.jp>までご一報お願い致します。以上、よろしくお願い申し上げます。世話人（五十音順）井上友喜尾國新一シャクマトフディミトリ野倉嗣紀平出耕一平田浩一藤田博司山内貴光 --- ウェブページ： http://www.math.sci.ehime-u.ac.jp/MTGSA.ja.html

1 0

論文募集：「プログラミングおよびプログラミング言語」特集
by Isao Sasano 11 Apr '17

11 Apr '17

皆様芝浦工業大学の篠埜です。論文誌「コンピュータソフトウェア」の特集「プログラミングおよびプログラミング言語」の論文募集のご案内です。 PPL2017の論文に限らず募集いたします。是非論文のご投稿をお願いいたします。 ----------------------------------------------------------------------- 論文募集：「プログラミングおよびプログラミング言語」特集 (論文投稿締切: 2017年6月16日(金) 17:00) http://www.jssst.or.jp/edit_news/detail/id=274 日本ソフトウェア科学会プログラミング論研究会は，毎年「プログラミングおよびプログラミング言語ワークショップ (PPL)」を開催しており，2017年3 月には第19回シンポジウム PPL2017 を開催しました．本「プログラミングおよびプログラミング言語」特集号は，PPL2017 に連動した企画であり，プログラミングに関する最先端の研究成果を掲載することを目的にしています．PPL2017 の発表論文を発展させた論文，PPL2017 での発表論文の中から推薦された論文（PPL2017 推薦論文），あるいはそれに限らず下記の対象分野に関連した論文を広く募集します．なお，PPL2017 との連携を強化するために，PPL2017 のプログラム共同委員長・篠埜功 (芝浦工業大学) 氏，番原睦則 (神戸大学) 氏を中心として特集号編集委員を構成しています．PPL2017 での発表論文を発展させた論文，および， PPL2017 推薦論文の査読にあたっては，PPL2017 の論文およびその査読結果を参考とさせていただきますので，迅速で一貫した査読が期待できます． <対象分野> プログラミングおよびプログラミング言語に関する研究成果 <募集論文> プログラミングおよびプログラミング言語に関する研究論文・解説論文・ソフトウェア論文 <執筆要領> 日本ソフトウェア科学会誌「コンピュータソフトウェア」の関連諸規定をご参照の上，投稿論文の PDF ファイルと「投稿メモ」を ppl2017si[at]org.kobe-u.ac.jp 宛てにお送りください．([at]を@に置換下さい) * PPL2017 で発表した論文を改訂して投稿する場合はその旨をお知らせください．学会誌関連諸規定は以下でご参照いただけます． http://www.jssst.or.jp/edit/kitei/ * レター論文による投稿を歓迎します． * レター論文は，査読者 1名による査読を行い，「照会後判定」は行わず，一度の査読で採否を判定します．刷り上がりで 6ページ以下の速報性を重視した論文です．レター論文を発展させたものは通常論文として投稿可能です． * 特集号に投稿された論文の査読基準は，一般投稿論文の査読基準と同じです． * 二重投稿にならないよう，十分ご注意下さい．（国際会議であっても，査読期間が重複する場合は二重投稿に該当します．） * 特集号への投稿に限り，日本ソフトウェア科学会の非会員による投稿も受け付けております．詳しくは上記より論文投稿規定をご覧ください． <スケジュール> 論文投稿締切り： 2017年6月16日(金) 17:00 特集号刊行予定： 2018年11月号査読プロセスの進行状況により掲載予定号に間に合わない場合があります．その場合でも特集論文として扱われます． <特集号編集委員> 青谷知幸 (東京工業大学)，馬谷誠二 (京都大学)，篠埜功 (芝浦工業大学)，番原睦則 (代表者，神戸大学) <企画母体> 日本ソフトウェア科学会プログラミング論研究会 <問合せ先> 篠埜功，番原睦則 (ppl2017si[at]org.kobe-u.ac.jp) ([at]は@で置き換えて下さい) ----------------------------------------------------------------------- 篠埜　功 -- Isao Sasano <sasano(a)sic.shibaura-it.ac.jp>

1 0

Talk by Marc Bagnol (13 Apr 11:00-)
by Tetsuya Sato 08 Apr '17

08 Apr '17

京都大学数理解析研究所の佐藤です。 4月13日11:00から、東京大学のMarc Bagnol氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 13 Apr, 2017 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: Marc Bagnol (JSPS Postdoctoral Fellow, University of Tokyo) Title: A Free Trace Construction and the Embedding Problem Abstract: The notion of traced category allows to model feedback situations in the language of category theory. Traces are ubiquitous in mathematics and serve as the basis for the categorical formulation of Girard's Geometry of Interaction. The notion was extended to partially-defined traces by Scott and Haghverdi, and a representation theorem was later shown: any partially traced category can be embedded in a fully traced one. A related problem we are currently investigating with some RIMS members is understanding when a monoidal category can be embedded into a traced one, or equivalently when it can be equipped with a partial trace. This "embedding problem" has already seen a few tentative solutions, conditions that are necessary but turned out not to be sufficient which I will present and discuss. I will also present a construction of a free trace for monoidal categories that both can be used to prove the representation theorem mentioned above (this was its original purpose) and gives an angle to look at the embedding problem.

1 0

Autumn school "Proof and Computation"
by Hajime Ishihara 07 Apr '17

07 Apr '17

Autumn school "Proof and Computation" Herrsching, Germany, 23rd to 26th September 2017 http://www.mathematik.uni-muenchen.de/~schwicht/pc17.php An international autumn school "Proof and Computation" will be held from 23rd to 26th September 2017 at Haus der bayerischen Landwirtschaft Herrsching in Herrsching near Munich. Its aim is to bring together young researchers in the field of Foundations of Mathematics, Computer Science and Philosophy. SCORE -------------------- - Predicative Foundations - Constructive Mathematics and Type Theory - Computation in Higher Types - Extraction of Programs from Proofs - Algorithmic Aspects in Financial Mathematics COURSES -------------------- - Mark Bickford on Constructive Analysis in NuPrl - Laura Crosilla on Foundations of Predicative Mathematics - Hajime Ishihara on Constructive Reverse Mathematics - Ulrich Kohlenbach on Proof Mining - Davide Rinaldi on Constructivising Transfinite Algebra - Andrei Rodin on Foundations of Axiomatic Mathematics - Gregor Svindland on Algorithmic Aspects in Financial Mathematics WORKING GROUPS -------------------- There will be an opportunity to form ad-hoc groups working on specific projects, but also to discuss in more general terms the vision of constructing correct programs from proofs. APPLICATIONS -------------------- Graduate or PhD students and young postdoctoral researches are invited to apply. Applications must be accompanied by a letter of recommendation, preferably from the thesis adviser, and should be sent to Chuangjie Xu (xu(a)math.lmu.de). DEADLINE for applications: **30th May 2017**. Applicants will be notified by 30th June 2017. FINANCIAL SUPPORT -------------------- The workshop is supported by the Udo Keller Stiftung (Hamburg), the CID (Computing with Infinite Data) programme of the European Commission and a JSPS core-to-core project. Successful applicants will be offered full-board accommodation for the days of the autumn school. There are no funds, however, to reimburse travel or further expenses, which successful applicants will have to cover otherwise. Klaus Mainzer Peter Schuster Helmut Schwichtenberg

1 0

Third Call for Papers ***** extended deadline ***** [LORI-VI] The Sixth International Conference on Logic, Rationality and Interaction
by Katsuhiko Sano 26 Mar '17

26 Mar '17

Third Call for Papers ***** extended deadline ***** [LORI-VI] The Sixth International Conference on Logic, Rationality and Interaction September 11-14, 2017, Hokkaido University, Sapporo, Japan http://golori.org/lori2017/ [About LORI] The International Conference on Logic, Rationality and Interaction (LORI) conference series aims at bringing together researchers working on a wide variety of logic-related topics that concern the understanding of rationality and interaction. The series aims at fostering a view of Logic as an interdisciplinary endeavour, and supports the creation of an East-Asian community of interdisciplinary researchers. [News] ****** Submission Deadline extended to Friday April 14 ****** [Call for Papers] We invite submission of contributed papers on any of the broad themes of LORI series; specific topics of interest include, but are not limited to, formal approaches to · agency · argumentation and agreement · belief representation · cooperation · belief revision and belief merging · strategic reasoning · games · decision making and planning · knowledge and action · epistemology · dynamics of informational attitudes · speech acts · knowledge representation · interaction · norms and normative systems · natural language · rationality · philosophy and philosophical logic · preference and utility · social choice · probability and uncertainty · social interaction · intentions, plans, and goals Submitted papers should be at most 12 pages long, with one additional page for references, in PDF format following the Springer LNCS style. Please submit your paper by Friday April 14, 2017, via EasyChair : http://easychair.org/conferences/?conf=lori6 . [Publication] Accepted papers will be collected as a volume in the FoLLI Series on Logic, Language and Information, and authors may be later invited to submit extended versions of their papers in a special issue of a prestigious journal. [Best Student Paper] The best student paper will be selected from the contributed student papers accepted for presentation at LORI VI, and be awarded the prize of 60,000 Japanese Yen (approximately 500 Euro). For more details, see http://golori.org/lori2017/award.html . [Website] For detailed conference information and registration, please visit http://golori.org/lori2017/ . [Invited Speakers] Mike Dunn: Indiana University, U.S.A. Alan Hájek: Australian National University, Australia Nina Gierasimczuk: Technical University of Denmark, Denmark Willemien Kets: Northwestern University, U.S.A Sara Negri: University of Helsinki, Finland Hiroakira Ono: JAIST, Japan [PC Chairs] Alexandru Baltag: University of Amsterdam, The Netherlands Jeremy Seligman: University of Auckland, New Zealand [Conference Organiser] Tomoyuki Yamada: Hokkaido University, Japan [Sponsors] LORI Tsinghua University - University of Amsterdam Joint Research Centre for Logic Hokkaido University [Contacts] Programme: The PC Chairs <lori6(a)easychair.org> Conference: Tomoyuki Yamada <tomoyuki.s.yamada(a)gmail.com>

1 0

Computability and Complexity in Analysis (CCA 2017): Final Call for Papers
by Daniel Graça 22 Mar '17

22 Mar '17

______________________________________________________________ Final Call for Papers Fourteenth International Conference on Computability and Complexity in Analysis (CCA 2017) http://cca-net.de/cca2017/ July 24-27, 2017, Daejeon, Republic of Korea (South Korea) Submission deadline: April 3, 2017 ______________________________________________________________ Topics * Computable analysis * Complexity on real numbers * Constructive analysis * Domain theory and analysis * Effective descriptive set theory * 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 Invited Speakers * Hee-Kap Ahn (Pohang, Republic of Korea) * Verónica Becher (Buenos Aires, Argentina) * Anders Hansen (Cambridge, UK) * Takayuki Kihara (Berkeley, USA) * Amaury Pouly (Max Planck Institute, Germany) * Linda Brown Westrick (Connecticut, USA) Funding Funding opportunities for student members of the Association for Symbolic Logic (ASL) are available. Applications should be directed to the Association for Symbolic Logic three months prior to the meeting, following the instructions here: http://www.aslonline.org/studenttravelawards.html Scientific Programme Committee * Johanna Franklin (Hempstead, USA) * Daniel Graça, chair (Faro, Portugal) * Vassilios Gregoriades (Turin, Italy) * Peter Hertling (Munich, Germany) * Gyesik Lee (Anseong, Republic of Korea) * Alexander Melnikov (Auckland, New Zealand) * Takako Nemoto (Ishikawa, Japan) * Arno Pauly (Brussells, Belgium) * Cristóbal Rojas (Santiago, Chile) * Frank Stephan (Singapore) * Klaus Weihrauch (Hagen, Germany) Organising Committee * Sunyoung Kim (Yonsei University, Republic of Korea) * Sewon Park (KAIST, Republic of Korea) * Martin Ziegler, chair (KAIST, Republic of Korea) Submissions Authors are invited to submit 1-2 pages abstracts in PDF format, including references via the following web page: https://easychair.org/conferences/?conf=cca2017 If full versions of papers are already available as technical report or arXiv version, then corresponding links should be added to the reference list. Final versions of abstracts might be distributed to participants in hardcopy and/or in electronic form. Dates * Submission deadline: April 3, 2017 * Notification of authors: May 1, 2017 * Final version: May 29, 2017 Conference Web Page http://cca-net.de/cca2017/ A co-located "Workshop on Real Verification" will take place on Friday, July 28, jointly organized by: * Gyesik Lee (Hankyong National University, Republic of Korea) * Martin Ziegler (KAIST, Republic of Korea) https://complexity.kaist.edu/CCA2017/workshop.html

1 0

RIMS共同研究（公開型）「証明論と証明活動」のご案内
by Katsumi Sasaki 16 Mar '17

16 Mar '17

みなさま　標記の共同研究として，以下の研究集会を開催します．　　　研究題目：証明論と証明活動　　　日程：2017年12月25日(月)〜27日(水) 　　　場所：京都大学数理解析研究所420号室　証明論・計算論・証明活動に関連する話題の講演を広く募集します．お忙しい時期かと思いますが，是非とも、講演・参加をご計画ください．　講演される学生の方には，旅費の援助があります．　詳細は， http://www.st.nanzan-u.ac.jp/info/sasaki/2017rims/rims2017.html で案内していく予定です．世話人：南山大学　佐々木克巳佐々木克巳 -- sasaki <sasaki(a)nanzan-u.ac.jp>

1 0

ITP 2017 - Final Call for Papers
by Nao Hirokawa 13 Mar '17

13 Mar '17

皆様 ITP 2017 の論文募集案内（最終）をお送り致します。ぜひ論文投稿をご検討下さい。廣川 (JAIST) ---------------------------------------------------------------------- FINAL CALL FOR PAPERS ITP 2017 8th International Conference on Interactive Theorem Proving Brasilia, Brazil September 26-29, 2017 http://itp2017.cic.unb.br SUBMISSION DEADLINES * April 3, 2017 (abstracts) * April 10, 2017 (full papers) GENERAL INFORMATION The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009. The eighth ITP conference, ITP 2017, will be held at Universidade de Brasilia, September 26-29, 2017. SCOPE OF CONFERENCE ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include but are not limited to the following: * formal aspects of hardware and software * formalizations of mathematics * improvements in theorem prover technology * user interfaces for interactive theorem provers * formalizations of computational models * verification of security algorithms * use of theorem provers in education * industrial applications of interactive theorem provers * concise and elegant worked examples of formalizations (proof pearls) PUBLICATION DETAILS The proceedings of the symposium will be published in the Springer's LNCS series. ** After the conference the authors of selected papers will be invited to submit revised papers for a special issue of the Journal of Automated Reasoning. ** PAPER SUBMISSIONS All submissions must be original, unpublished, and not submitted concurrently for publication elsewhere. Furthermore, when appropriate, submissions are expected to be accompanied by verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used. Submissions should be no more than 16 pages in length and are to be submitted in PDF via EasyChair at the following address: https://easychair.org/conferences/?conf=itp2017 Submissions must conform to the LNCS style in LaTeX. Authors of accepted papers are expected to present their paper at the conference and will be required to a sign copyright release form. In addition to regular papers, described above, there will be a rough diamond section. Rough diamond submissions are limited to 6 pages and may consist of an extended abstract. They will be refereed and be expected to present innovative and promising ideas, possibly in an early form and without supporting evidence. Accepted diamonds will be published in the main proceedings and will be presented as short talks. IMPORTANT DATES Abstract submission deadline: April 3, 2017 Full paper submission deadline: April 10, 2017 Author notification: June 2, 2017 Camera-ready papers: June 30, 2017 Workshops & Tutorials: September 23-25, 2017 Conference: September 26-29, 2017 INVITED SPEAKERS Moa Johansson, Chalmers University of Technology, Sweden Leonardo de Moura, Microsoft Research Cezary Kaliszyk, Universitaet Innsbruck, Austria (joint with TABLEAUX and FroCos) Katalin Bimbo, University of Alberta, Canada (joint with TABLEAUX and FroCos) Jasmin Blanchette, Inria and LORIA, Nancy, France (joint with TABLEAUX and FroCos) WORKSHOPS AND TUTORIALS There will be a three-day programme of four workshops and four tutorials from 23-25 September. Workshops: 12th Logical and Semantic Frameworks with Applications (LSFA 2017) Sandra Alves, Renata Wassermann, Flavio L. C. de Moura 23 and 24 September 2017 Proof eXchange for Theorem Proving (PxTP) Catherine Dubois, Bruno Woltzenlogel Paleo 23 and 24 September 2017 EPS - Encyclopedia of Proof Systems Giselle Reis, Bruno Woltzenlogel Paleo 24 and 25 September 2017 DaLi - Dynamic Logic: new trends and applications Mario Benevides, Alexandre Madeira 24 September 2017 Tutorials: General methods in proof theory for modal and substructural logics Bjoern Lellmann, Revantha Ramanayake 23 September 2017 From proof systems to complexity bounds Anupam Das 24 September 2017 Proof Compressions and the conjecture NP =3D PSPACE Lew Gordeev, Edward Hermann Haeusler 25 September 2017 PVS for Computer Scientists Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato 25 September 2017 Details will be published in separate calls and on the conference website. PROGRAM COMMITTEE CHAIRS Mauricio Ayala-Rincon, U. Brasilia Cesar Munoz, NASA PROGRAM COMMITTEE Maria Alpuente, T.U. Valencia Vander Alves, U. Brasilia June Andronick, Data61, CSIRO, UNSW Jeremy Avigad, Carnegie Mellon U. Sylvie Boldo, INRIA LRI Ana Bove, Chalmers & Gothenburg U. Adam Chlipala, MIT Gilles Dowek, INRIA, ENS Cachan Aaron Dutle, NASA Amy Felty, U. Ottawa Marcelo Frias, I.T. Buenos Aires Ruben Gamboa, U. Wyoming Herman Geuvers, Radboud U. Elsa Gunter, U. Illinois U.C. John Harrison, Intel Corporation Nao Hirokawa, JAIST Matt Kaufmann, U. Texas Austin Mark Lawford, McMaster U. Andreas Lochbihler, ETH Zurich Assia Mahboubi, INRIA Panagiotis Manolios, Northeastern U. Gopalan Nadathur, U. Minnesota Keiko Nakata, SAP Potsdam Adam Naumowicz, U. Bialystok Tobias Nipkow, T.U. Munich Scott Owens, U. Kent Sam Owre, SRI Lawrence Paulson, U. Cambridge Leila Ribeiro, U.F. Rio Grande do Sul Claudio Sacerdoti Coen, U. Bologna Augusto Sampaio, U.F. Pernambuco Monika Seisenberger, Swansea U. Christian Sternagel, U. Innsbruck Sofiene Tahar, Concordia U. Christian Urban, King's College London Josef Urban, Czech T.U. Prague CONTACT INFORMATION itp2017(a)easychair.org http://itp2017.cic.unb.br

1 0

[FINAL CALL FOR PAPERS] TABLEAUX 2017, University of Brasilia, Brazil, September 25-28, 2017
by Katsuhiko Sano 13 Mar '17

13 Mar '17

************************************************************************ FINAL CALL FOR PAPERS TABLEAUX 2017 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods University of Brasilia, Brazil September 25-28, 2017 Deadlines: 18 Apr 2017 (abstract), 25 Apr 2017 (paper) http://tableaux2017.cic.unb.br/ GENERAL INFORMATION TABLEAUX is the main international conference at which research on all aspects, theoretical foundations, implementation techniques, systems development and applications, of the mechanization of tableau-based reasoning and related methods is presented. As the first TABLEAUX workshop was held in Lautenbach in 1992, this year's conference will include special events celebrating 25 years of TABLEAUX. The conference will be held in Brasilia from 25-28 September 2017. It will be co-located with both the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) and the 8th International Conference on Interactive Theorem Proving (ITP 2017). TOPICS Tableau methods offer a convenient and flexible set of tools for automated reasoning in classical logic, extensions of classical logic, and a large number of non-classical logics. For large groups of logics, tableau methods can be generated automatically. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis. Topics of interest include but are not limited to: * tableau methods for classical and non-classical logics (including first-order, higher-order, modal, temporal, description, hybrid, intuitionistic, substructural, relevance, non-monotonic logics) and their proof-theoretic foundations; * related methods (SMT, model elimination, model checking, connection methods, resolution, BDDs, translation approaches); * sequent calculi and natural deduction calculi for classical and non-classical logics, as tools for proof search and proof representation; * flexible, easily extendable, light weight methods for theorem proving; * novel types of calculi for theorem proving and verification in classical and non-classical logics; * systems, tools, implementations, empirical evaluations and applications (provers, logical frameworks, model checkers, ...); * implementation techniques (data structures, efficient algorithms, performance measurement, extensibility, ...); * extensions of tableau procedures with conflict-driven learning, generation of proofs; compact (or humanly readable) representation of proofs; * decision procedures, theoretically optimal procedures; * applications of automated deduction to mathematics, software development, verification, deductive and temporal databases, knowledge representation, ontologies, fault diagnosis or teaching. We also welcome papers describing applications of tableau procedures to real world examples. Such papers should be tailored to the tableau community and should focus on the role of reasoning, and logical aspects of the solution. CELEBRATING 25 YEARS To celebrate 25 years TABLEAUX the conference will include a special session of invited talks by: Reiner Haehnle Technische Universitaet Darmstadt, Germany Wolfgang Bibel Technische Universitaet Darmstadt, Germany INVITED SPEAKERS: Carlos Areces FaMAF - Universidad Nacional de Cordoba, Argentina Katalin Bimbo University of Alberta, Canada (with FroCoS and ITP) Jasmin Blanchette Inria and LORIA, Nancy, France (with FroCoS and ITP) Cezary Kaliszyk Universitaet Innsbruck, Austria (with FroCoS and ITP) WORKSHOPS AND TUTORIALS There will be a three-day programme of four workshops and four tutorials from 23-25 September. Workshops: 12th Logical and Semantic Frameworks with Applications (LSFA 2017) Sandra Alves, Renata Wassermann, Flavio L. C. de Moura 23 and 24 September 2017 Proof eXchange for Theorem Proving (PxTP) Catherine Dubois, Bruno Woltzenlogel Paleo 23 and 24 September 2017 EPS - Encyclopedia of Proof Systems Giselle Reis, Bruno Woltzenlogel Paleo 24 and 25 September 2017 DaLi - Dynamic Logic: new trends and applications Mario Benevides, Alexandre Madeira 24 September 2017 Tutorials: General methods in proof theory for modal and substructural logics Bjoern Lellmann, Revantha Ramanayake 23 September 2017 From proof systems to complexity bounds Anupam Das 24 September 2017 Proof Compressions and the conjecture NP = PSPACE Lew Gordeev, Edward Hermann Haeusler 25 September 2017 PVS for Computer Scientists Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato 25 September 2017 Details will be published in separate calls and on the conference website. POSTER SESSION There will be a joint poster session for TABLEAUX 2017, FroCos 2017, and ITP 2017. The session is intended for descriptions of work in progress, student projects and relevant research being published elsewhere. The deadline for posters submission is June 15, 2017. More details can be found at http://tableaux2017.cic.unb.br/#postersession. PUBLICATION DETAILS The conference proceedings will published in the Springer LNAI/LNCS series, as in previous editions. SUBMISSIONS Submissions are invited in two categories: A Research papers, which describe original theoretical research, original algorithms, or applications, with length up to 15 pages. B System descriptions, with length up to 9 pages. Submissions will be reviewed by the PC, possibly with the help of external reviewers, taking into account readability, relevance and originality. For category A, theoretical results and algorithms must be original, and not submitted for publication elsewhere. Submissions will be reviewed taking into account correctness, theoretical elegance, and possible implementability. For category B submissions, a working implementation must be accessible via the internet, which includes sources. The aim of a system description is to make the system available in such a way that users can use it, understand it, and build on it. Accepted papers in both categories will be published in the conference proceedings. Papers must be edited in LaTeX using the llncs style and must be submitted electronically as PDF files via the EasyChair system: https://easychair.org/conferences/?conf=tableaux2017. For all accepted papers at least one author is required to attend the conference and present the paper. A paper title and a short abstract of about 100 words must be submitted before the paper submission deadline. Further information about paper submissions will be made available at the conference website. Be aware that neither plagiarism, nor self-plagiarism, nor duplicate publication is acceptable. Formatting instructions and the LNCS style files can be obtained via http://www.springer.com/br/computer-science/lncs/conference-proceedings-gui… BEST PAPER AWARD The TABLEAUX 2017 Best Paper Award will be presented to the best submission nominated and chosen by the Program Committee among the accepted papers. The eligibility criteria will place emphasis on the originality and significance of the contribution, but readability and the overall technical quality, including correctness and completeness of results, will also be considered. The TABLEAUX Best Paper Award was established in 2015 and is a permanent initiative of TABLEAUX. IMPORTANT DATES 18 Apr 2017 Abstract submission 25 Apr 2017 Paper submission 8 Jun 2017 Notification of paper decisions 3 Jul 2017 Camera-ready papers due 23-25 Sep 2017 Workshops & Tutorials 25-28 Sep 2017 TABLEAUX Conference PROGRAM COMMITTEE Peter Baumgartner National ICT Australia, Canberra Maria Paola Bonacina Universita degli Studi di Verona Laura Bozzelli Universidad Politecnica de Madrid Torben Brauener Roskilde University Serenella Cerrito Ibisc, Universite d'Evry Val d'Essonne Agata Ciabattoni Technische Universitaet Wien Clare Dixon University of Liverpool Pascal Fontaine LORIA, INRIA, Universite de Lorraine Didier Galmiche LORIA, Universite de Lorraine Martin Giese Universitetet i Oslo Laura Giordano DISIT, Universita del Piemonte Orientale Rajeev Gore The Australian National University Volker Haarslev Concordia University George Metcalfe Universitaet Bern Angelo Montanari Universita degli Studi di Udine Barbara Morawska Technische Universitaet Dresden Boris Motik University of Oxford Leonardo de Moura Microsoft Research Neil Murray SUNY at Albany Claudia Nalon Universidade de Brasilia Linh Anh Nguyen Uniwersytet Warszawski Hans de Nivelle Uniwersytet Wroclawski Nicola Olivetti LSIS, Aix-Marseille Universite Jens Otten Universitetet i Oslo Valeria de Paiva Nuance Communications Nicolas Peltier Centre National de la Recherche Scientifique, Laboratoire d'Informatique de Grenoble Elaine Pimentel Universidade Federal do Rio Grande do Norte Giselle Reis Carnegie Mellon University-Qatar Philipp Ruemmer Uppsala Universitet Katsuhiko Sano Hokkaido University Renate Schmidt The University of Manchester Cesare Tinelli The University of Iowa Alwen Tiu Nanyang Technological University David Toman University of Waterloo Josef Urban Ceske vysoke uceni technicke v Praze LOCAL CONFERENCE ORGANIZATION COMMITTEE Claudia Nalon, Universidade de Brasilia, Brazil Daniele Nantes Sobrinho, Universidade de Brasilia, Brazil Elaine Pimentel, Universidade Federal do Rio Grande do Norte, Brazil Joao Marcos, Universidade Federal do Rio Grande do Norte, Brazil CONFERENCE CHAIR Claudia Nalon, University of Brasilia, Brazil PC CHAIRS Claudia Nalon, University of Brasilia, Brazil Renate Schmidt, The University of Manchester, UK

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml