Logic-ml

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

1792 discussions

Talk by Thomas Seiller (October 3rd, 11.00-)
by Kazushige TERUI 01 Oct '19

01 Oct '19

みなさま今週木曜日に京都大学にてThomas Seillerさんによるご講演があります。詳細は下記の通りです。よろしければぜひご参加ください。京都大学数理解析研究所照井一成 ========== Time: 11:00-12:00, October 3rd, 2019 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) Speaker: Thomas Seiller (LIPN, University of Paris 13) Title: Dynamical systems and computational complexity Abstract: Based on previous work on semantics of linear logic which used the notion of “graphing”, I started to study how these mathematical objects, which generalize partial dynamical systems, can shed new light on computability. Focussing on questions of complexity, Pellissier and I recently showed how interpreting programs as dynamical systems can lead to an abstract method for proving lower bounds that capture several previously known results. More importantly, the method can be refined to strengthen the previously best-known partial result towards settling the Ptime vs NC question negatively. Building on some realisability construction for linear logic capturing standard complexity classes, this leads to wonder about how much can be learned from dynamical systems, and if the field can provide new insights on important questions such that “Is Ptime equal to Logspace?”.

1 0

不完全性定理入門集中講義のご案内
by Toshio Suzuki 26 Sep '19

26 Sep '19

不完全性定理入門集中講義のご案内（重複して受け取られた折はご容赦ください）お世話になっております。首都大学東京の鈴木登志雄です。さて１０月・１１月に首都大学東京理学研究科数理科学専攻では，東京工業大学の鹿島先生に不完全性定理入門の集中講義をしていただきます。最終日には証明可能性論理にもふれていただける見込みです。公式にオープンセミナーとうたっているわけではありませんが，当専攻ではこの種の集中講義に数名程度まで学外の院生等が聴きに来ても黙認する慣習のようです。お近くに関心のありそうな方がいらっしゃいましたら、お知らせいただければ幸いです。 %%%%%%% ここから＊＊担当者鹿島亮先生（東京工業大学情報理工学院准教授）　＊＊授業科目名応用数理特別講義２　　　(数理科学専攻　前期課程：Ｒ００８１) タイトル不完全性定理への現代的な入門場所　首都大学東京（南大沢キャンパス）８号館６階６１０時期１０月１０日（木），１７日（木），３１日（木），１１月７日（木）の１４：４０－１７：５０（途中休憩あり）当専攻での連絡係鈴木登志雄 toshio-suzuki[atmark]tmu.ac.jp 概要ゲーデルの不完全性定理は数理論理学における重要な基本定理でありコンピュータサイエンスや哲学などにも多大な影響を与えているが，しばしば誤解もされている．本講義の目的は詳細な議論によってこの定理の数学的な正しい理解を与えることである．ゲーデルの原論文(1931)を忠実になぞるのではなく，本講義ではペアノ算術を主な対象としてより現代的な証明を行う。教科書：田中一之編『ゲーデルと２０世紀の論理学（３）不完全性定理と算術の体系』東京大学出版会 (2007) pp.37-114 所収，鹿島亮「第一不完全性定理と第二不完全性定理」。 %%%%%%% ここまで首都大学東京南大沢キャンパスへの交通 http://www.tmu.ac.jp/university/campus_guide/access.html 同・構内図 http://www.tmu.ac.jp/university/campus_guide/map.html -- 鈴木登志雄首都大学東京理学研究科数理科学専攻 toshio-suzuki(a)tmu.ac.jp

1 0

JAIST Logic Seminar Series - Beckmann 教授講演のお知らせ (10月4日)
by Nao Hirokawa 26 Sep '19

26 Sep '19

皆様１０月４日（金）に北陸先端科学技術大学院大学で行われます Arnold Beckmann 教授の講演のお知らせです。皆様、どうぞ奮ってご参加ください。廣川直 (JAIST) ----------------------------------------------------------------------- * JAIST Logic Seminar Series * Date: October 4 (Fri), 2019, 15:00 - 16:30 Place: I-65 (seminar room on 6F of IS Building III) at JAIST (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Arnold Beckmann (Swansea University) Title: Consistency of equational theories and the separation problem for bounded arithmetic Abstract: Consistency statements of formal theories have been considered as candidates for separating theories of bounded arithmetic. The most promising ones are given by consistency statements of certain equational theories. The starting points for this line of research are results by Buss and Ignjatovic 1995 [Unprovability of consistency statements in fragments of bounded arithmetic, APAL 1995, 74: 221--244], which shows that the consistency of an induction free version of the equational theory PV is not provable in the bounded arithmetic theory S^1_2, and Beckmann 2002 [Proving consistency of equational theories in bounded arithmetic. JSL 2002, 67: 279--296] which shows that the consistency of a further restricted induction free version of PV is provable in S^1_2. We review those results and in particular state them precisely. We then explain the progress that has been made over recent years to narrow the gap between provability and unprovability, and the potential research programme that is related to this question.

1 0

締切延長: フォーマルアプローチ特集論文募集のご案内
by ken.mano.eh＠hco.ntt.co.jp 18 Sep '19

18 Sep '19

皆様， IEICE フォーマルアプローチ特集ですが，多くの方に原稿をご投稿いただきたく，投稿締め切りを 2019 年 10 月 8 日まで延長いたしました．投稿をご検討いただきますよう，なにとよろしくお願い致します．真野 =========================================================================== フォーマルアプローチ特集論文募集電子情報通信学会論文誌英文 ED 分冊フォーマルアプローチ特集編集委員会フォーマルアプローチ（形式手法・形式技法・形式理論）は，情報システムや組込みシステムの設計開発における信頼性向上の鍵となる重要な基盤です．これまで，設計対象のモデル化，要求分析と仕様記述，コード自動生成，テストと検証，保守と再利用などに関する技術と理論的知見を生み出してきました．近年の情報技術の進展に伴う対象領域の拡大に伴い，フォーマルアプローチは従来にも増して多様な分野で用いられるようになり，ますます発展しています．本小特集は，情報システムや組込みシステムの設計・運用におけるフォーマルアプローチについて，基礎理論から応用まで，幅広い研究を対象にしています．個別の対象領域に特化したケーススタディから，分野横断的な手法や理論まで，様々な方面から，フォーマルアプローチ研究に携わる若手研究者を奨励するとともに，この分野の研究が更に発展することを目指しております．奮って御投稿下さいますよう御案内申し上げます． 1. 対象分野主な対象は以下のとおりですが，これに限らず，「情報システムや組込みシステム及びそれをとりまく環境を定式化した上で，そのシステムの振舞いの解析や性質の導出を厳密に行い，設計・運用に関わる種々の問題の解決を図る」ことを目指した論文を広く募集します． - 基礎理論：システムの構造や振舞いの形式記述・検証に関する基礎理論 - 形式技法：ソフトウェア，ハードウェア，ネットワークなどのシステムに対する体系だった記述・検証技法 - 形式ツール：モデル検査器や定理証明器など，形式手法に基づくツール - 応用：情報システムや組込システム，回路系，情報セキュリティ，車載システム，人工知能・機械学習システム，マルチエージェントなどへの形式手法の適用事例 - 教育：教育事例 2. 論文の執筆と取扱い論文 (一般論文)，レター，及びサーベイ論文を募集します．投稿規程等は電子情報通信学会の英文誌の規程と同じです．以下の規程を御参照下さい． "The Information for Authors" (IEICE Transactions on Information and Systems) http://www.ieice.org/eng/shiori/mokuji_iss.html 3. 主なスケジュール論文投稿締切 2019 年 10 月 8 日 (火) 23:59 JST (延長いたしました) 第一回判定通知予定 2019 年 12 月 6 日 (金) 初回修正締切 2020 年 1 月 31 日 (金) 最終判定通知予定 2020 年 3 月 20 日 (金) 発行予定 2020 年 8 月号 4. 投稿方法本特集では，電子投稿のみを受付けます．論文を下記の web page から投稿して下さい．初期投稿時に，編集可能な論文本体 (TeX/Word)，図，著者の写真，biography も投稿する必要があります． https://review.ieice.org/regist/regist_baseinfo_e.aspx 投稿の際には以下の項目を選択してください． "Journal/Section" -> "[Special FO] Formal Approaches" 同時に WEB 上で著作権譲渡手続きができます．投稿手続きについて御不明な点がございましたら，問合先まで御連絡下さい． 5. 掲載料招待論文を含むすべての著者は，論文が採録となった場合，2020 年 4 月頃に掲載料をお支払い頂くことになります．2020 年 5 月 15 日までに支払いが完了しない場合には，採録取り消しとなります． 6. オープン化，オープンアクセスオプション・オープン化：2017年1月号以降に掲載された電子情報通信学会英文論文誌Ｄのすべての論文を，J-STAGEを通じて全世界の読者へ公開しています．・2020年1月号以降に掲載される論文には，電子情報通信学会の多くの論文誌で適用することができるオープンアクセスオプションを適用することができなくなります．（オープン化は，2020年1 月以降も継続する予定です．）・オープン化とオープンアクセスオプションに関する詳細は，"Information for Authors"　(http://www.ieice.org/eng/shiori/mokuji_iss.html) を御参照下さい．・オープン化とオープンアクセスオプションに関しては，予告なく変更されることがあります． 7. 特集編集委員会委員長：真野健(NTT) 幹事：石川冬樹(情報研)，横川智教（岡山県立大）委員：青木利晃(北陸先端大)，青木善貴（日本ユニシス），來間啓伸(日立)，小林孝一(北大)，立石孝彰(日本IBM)，土屋達弘(阪大)，山口真悟(山口大) 8. 問合せ先本特集のホームページ: (和文) http://www.brl.ntt.co.jp/people/mano/fa2019/jp/ (英文) http://www.brl.ntt.co.jp/people/mano/fa2019/ 真野健 NTT コミュニケーション科学基礎研究所〒243-0198 神奈川県厚木市森の里若宮 3-1 ken.mano.eh(a)hco.ntt.co.jp =============================================================== CALL FOR PAPERS Special Section on Formal Approaches The IEICE Transactions on Information and Systems announces a forthcoming special section on Formal Approaches to be published in August 2020. Formal methods and techniques play a key role in designing and developing highly reliable information systems and embedded systems. The last decades have seen various new techniques and profound theoretical results using formal methods in surprisingly many fields such as modeling, requirements analysis, specification, automatic generation of codes, testing, verification, and maintenance. They are rapidly extending their application domains as a result of the recent growth of information and communication technologies. The Special Section on Formal Approaches aims at stimulating research on formal approaches to information systems and embedded systems, ranging from fundamental theory to practical applications. Our emphasis is put on the cross-fertilization of related research fields and encouragement of young researchers. Topics: The major topics are listed below, but we solicit submissions in all areas of formal approaches, i.e., first to formalize information systems, embedded systems, and their environment, next to analyze their behavior and to derive their properties rigorously, and then to solve various problems in designing and managing the systems. - Theoretical foundations: all aspects of theory related to formal description and verification for structure and behavior of systems. - Formal techniques: techniques for mainly describing and analyzing systems, such as software, hardware and networks. - Formal tools: tools based on formal methods such as model checkers, theorem provers, and static and dynamic analyzers. - Applications: practical experiences of applying formal methods to information systems, embedded systems, circuits, security, AI systems, machine learning systems, multi-agent systems, automotive systems, etc. - Education: education on formal methods. Submission Instructions: The deadline for submission is Oct 8, 2019, 23:59 JST(GMT+9) (Extended). Manuscripts should be carefully prepared according to the guideline in the "Information for Authors" (available at http://www.ieice.org/eng/shiori/mokuji_iss.html). The preferred length of the manuscript is 8 pages. Only electronic submission through the web page is accepted. Submit a complete paper and transfer copyright of the paper using the IEICE Web site https://review.ieice.org/regist/regist_baseinfo_e.aspx Authors should choose the [Special FO] Formal Approaches" as a "Journal/Section" on the online screen. Editorial Committee: Guest Editor-in-Chief: Ken Mano (NTT Communication Science Laboratories) Guest Editors: Fuyuki Ishikawa (National Institute of Informatics) Tomoyuki Yokogawa (Okayama Prefectural University) Members: Toshiaki Aoki (JAIST) Yoshitaka Aoki (Nihon Unisys) Koichi Kobayashi (Hokkaido University) Hironobu Kuruma (Hitachi, Ltd.) Takaaki Tateishi (IBM Japan) Tatsuhiro Tsuchiya (Osaka University) Shingo Yamaguchi (Yamaguchi University) Further information may be obtained from the web page at: http://www.brl.ntt.co.jp/people/mano/fa2019/ All inquiries should be sent to the guest editor in chief: Ken Mano NTT Communication Science Laboratories 3-1 Morinosato Wakamiya Atsugi Kanagawa 243-0198 Japan E-mail: ken.mano.eh(a)hco.ntt.co.jp Important Dates: Submission Deadline: Oct 8, 2019 23:59 JST (GMT+9) [Extended] First Notification: Dec 6, 2019 Revised Version Deadline: Jan 31, 2020 Final Notification: Mar 20, 2020 Important Notice. (1) At least one of the authors must be an IEICE member when the manuscript is submitted for review. For the application of IEICE membership, visit http://www.ieice.org/eng/member/OM-appli.html (2) When a paper has been accepted for publication, the authors are required to pay the page charges covering part of the cost of publication. Please carefully read the submission guideline at http://www.ieice.org/eng/shiori/mokuji_iss.html (3) Upon accepted for publication, all authors, including authors of invited papers, should pay the page charges covering partial cost of publication around April, 2020. If payment is not completed by May 15, 2020, your manuscript will be handled as rejection. (4) [Open Access Publishung, Open Access Option] ・Open Access Publishing: Since January 2017, all papers of the IEICE Transactions on Information and Systems stored in J-STAGE that include all papers published from January 2017 have been opened to all reader in the world through J-STAGE. ・Open Access Option for many transactions in IEICE will not be applied to papers in January 2020 issue and following issues of the IEICE Transactions on Information and Systems. (Open Access Publishing will be continued after January 2020.) ・For details on Open Access Publishing and Open Access Options, please carefully refer to “The Information for Authors” (http://www.ieice.org/eng/shiori/mokuji_iss.html). ・Note that these rules may be changed without notice.

1 0

FLOPS 2020 First Call for papers
by Keisuke Nakano 18 Sep '19

18 Sep '19

logic-mlの皆様，東北大学の中野です． FLOPS 2020 の論文募集のご案内です． 4月に秋田で4/23-25に開催予定です．ふるってご投稿ください． # ETAPSのmain conference(4/27-5/1)には重ならない日程での開催ですのでぜひご検討ください． -- 中野圭介東北大学電気通信研究所 ksk(a)riec.tohoku.ac.jp FIRST Call For Papers FLOPS 2020: 15th International Symposium on Functional and Logic Programming =============================== 23-25 April, 2020, Akita, Japan https://www.ipl.riec.tohoku.ac.jp/FLOPS2020/ Writing down detailed computational steps is not the only way of programming. An alternative, being used increasingly in practice, is to start by writing down the desired properties of the result. The computational steps are then (semi-)automatically derived from these higher-level specifications. Examples of this declarative style of programming include functional and logic programming, program transformation and rewriting, and extracting programs from proofs of their correctness. FLOPS aims to bring together practitioners, researchers and implementors of the declarative programming paradigm, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming. *** Scope *** FLOPS solicits original papers in all areas of the declarative programming: * functional, logic, functional-logic programming, rewriting systems, formal methods and model checking, program transformations and program refinements, developing programs with the help of theorem provers or SAT/SMT solvers, verifying properties of programs using declarative programming techniques; * foundations, language design, implementation issues (compilation techniques, memory management, run-time systems, etc.), applications and case studies. FLOPS promotes cross-fertilization among different styles of declarative programming. Therefore, research papers must be written to be understandable by the wide audience of declarative programmers and researchers. In particular, each submission should explain its contributions in both general and technical terms, clearly identifying what has been accomplished, explaining why it is significant for its area, and comparing it with previous work. Submission of system descriptions and declarative pearls are especially encouraged. *** Submission *** Submissions should fall into one of the following categories: * Regular research papers: they should describe new results and will be judged on originality, correctness, and significance. * System descriptions: they should describe a working system and will be judged on originality, usefulness, and design. * Declarative pearls: new and excellent declarative programs or theories with illustrative applications. System descriptions and declarative pearls must be explicitly marked as such in the title. Submissions must be unpublished and not submitted for publication elsewhere. Work that already appeared in unpublished or informally published workshops proceedings may be submitted. See also ACM SIGPLAN Republication Policy, as explained on the web at http://www.sigplan.org/Resources/Policies/Republication. Submissions must be written in English and can be up to 15 pages excluding references, though system descriptions and pearls are typically shorter. The formatting has to conform to Springer's guidelines. Regular research papers should be supported by proofs and/or experimental results. In case of lack of space, this supporting information should be made accessible otherwise (e.g., a link to an anonymized Web page or an appendix, which does not count towards the page limit). However, it is the responsibility of the authors to guarantee that their paper can be understood and appreciated without referring to this supporting information; reviewers may simply choose not to look at it when writing their review. FLOPS 2020 will employ a lightweight double-blind reviewing process. To facilitate this, submitted papers must adhere to two rules: 1. author names and institutions must be omitted, and 2. references to authors' own related work should be in the third person (e.g., not "We build on our previous work …" but rather "We build on the work of …"). The purpose of this process is to help the reviewers come to an initial judgement about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing the paper more difficult (e.g., important background references should not be omitted or anonymized). In addition, authors should feel free to disseminate their ideas or draft versions of their paper as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas. Papers should be submitted electronically at EasyChair which will be available soon from the Web Site of FLOPS 2020. *** Proceedings *** The proceedings will be published by Springer International Publishing in the Lecture Notes in Computer Science (LNCS) series. *** Important Dates *** 15 November 2019 (AoE): Abstract submission 22 November 2019 (AoE): Submission deadline 24 January 2020: Author notification 16 February 2020: Camera ready due 23-25 April 2020: FLOPS Symposium *** Organizers *** Keisuke Nakano Tohoku University, Japan (PC Co-Chair, General Chair) Kostis Sagonas Uppsala University, Sweden (PC Co-Chair) Kazuyuki Asada Tohoku University, Japan (Local Co-Chair) Ryoma Sin'ya Akita University, Japan (Local Co-Chair) Katsuhiro Ueno Tohoku University, Japan (Local Co-Chair) *** Contact Address *** flops2020 _AT_ easychair.org -------------------------------------------------------------------------------

1 0

RIMS共同研究（公開型）「証明論とその周辺」のご案内
by Yoshihito Tanaka 12 Sep '19

12 Sep '19

（複数のメーリングリストにお送りしています．重複してお受け取りの際はご容赦ください）皆様，九州産業大学の田中義人と申します．例年行われている証明論を中心とした研究集会を，今年度はRIMS共同研究（公開型）「証明論とその周辺」として，下記の要領で開催する予定です．日程：2019年12月24日（火）-12月26日（木）場所：京都大学15号館201教室懇親会（予定）：12月24日（火）会費：4000円程度 Webページ：http://www.ip.kyusan-u.ac.jp/J/ms/event/pt19/proof_theory_2019.html 参加を希望される方は，11月8日（金）までに，ytanaka(a)ip.kyusan-u.ac.xn--jp,-9b4b342t 以下の項目をご連絡ください．・お名前・所属・e-mailアドレス・講演の有無．講演有の場合は，タイトルおよび，講演時間や講演日時等のご希望・旅費援助希望の有無（申し込み状況によってはご希望に添えない場合があります）・懇親会参加希望の有無多くの皆様のご講演・ご参加をお待ちしております． ********************************* 田中義人九州産業大学経済学部 813-8503 福岡市東区松香台2-3-1 092-673-5216 (直通) e-mail: ytanaka(a)ip.kyusan-u.ac.jp *********************************

1 0

LFCS 2020 CFP, deadline extension till Sept 16
by Hajime Ishihara 09 Sep '19

09 Sep '19

Symposium on LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS’20), Deerfield Beach, Florida, January 4-7, 2020. LFCS Steering Committee: Anil Nerode, (Ithaca, NY, General Chair); Stephen Cook (Toronto); Dirk van Dalen (Utrecht); Yuri Matiyasevich (St.Petersburg, Russia); Samuel Buss (San Diego); Gerald Sacks (Cambridge, MA); Andre Scedrov (Philadelphia, PA); Dana Scott, (Pittsburgh, PA - Berkeley, CA). LFCS topics of interest include, but are not limited to: constructive mathematics and type theory; homotopy type theory; logic, automata, and automatic structures; computability and randomness; logical foundations of programming; logical aspects of computational complexity; parameterized complexity; logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; logical methods in program specification and extraction; domain theory logics; logical foundations of database theory; equational logic and term rewriting; lambda and combinatory calculi; categorical logic and topological semantics; linear logic; epistemic and temporal logics; intelligent and multiple agent system logics; logics of proof and justification; nonmonotonic reasoning; logic in game theory and social software; logic of hybrid systems; distributed system logics; mathematical fuzzy logic; system design logics; other logics in computer science. LFCS’20 Program Committee: Sergei Artemov (New York, NY) - PC Chair; Eugene Asarin (Paris); Steve Awodey (Pittsburgh, PA); Lev Beklemishev (Moscow); Andreas Blass (Ann Arbor, MI); Samuel Buss (San Diego, CA); Robert Constable (Ithaca, NY); Thierry Coquand (Göteborg); Valeria de Paiva (Cupertino, CA); Ruy de Queiroz (Recife); Nachum Dershowitz (Tel Aviv); Melvin Fitting (New York, NY); Sergey Goncharov (Novosibirsk); Denis Hirschfeldt (Chicago, IL); Rosalie Iemhoff (Utrecht); Hajime Ishihara (JAIST - Kanazawa); Bakhadyr Khoussainov (Auckland); Roman Kuznets (Vienna); Daniel Leivant (Bloomington, IN); Robert Lubarsky (Boca Raton, FL); Victor Marek (Lexington, KY); Lawrence Moss (Bloomington, IN); Anil Nerode (Ithaca, NY) - General LFCS Chair; Hiroakira Ono (JAIST - Kanazawa); Alessandra Palmigiano (Delft); Ramaswamy Ramanujam (Chennai); Michael Rathjen (Leeds); Helmut Schwichtenberg (Munich); Sebastiaan Terwijn (Nijmegen). Submission details. Proceedings will be published in the Springer LNCS series. Submissions should be made electronically via easychair. Submitted papers must be in pdf/12pt format and of no more than 15 pages, present work not previously published, and must not be submitted concurrently to another conference with refereed proceedings. Submission page: https://easychair.org/conferences/?conf=lfcs2020 LFCS issues the best student paper award named after John Barkley Rosser Sr. (1907-1989), a prominent American logician with fundamental contributions in both Mathematics and Computer Science. Important Dates. Submissions deadline: midnight September 16, 2019, any time zone (extended!) Notification: October 10, 2019. Symposium dates: January 4–7, 2020. Local Arrangements. The venue of LFCS 2020 will be the spectacular Wyndham Deerfield Beach Resort, 2096 NE 2nd Street, Deerfield Beach, Florida 33441. Website: http://www.wyndhamdeerfieldresort.com LFCS’20 Local Organizing Committee Chair is Robert Lubarsky, Florida Atlantic University. Further Information about LFCS’20: https://lfcs.ws.gc.cuny.edu/lfcs-2020/ Sponsorships: The US National Science Foundation (pending), Association for Symbolic Logic, Cornell University, The City University of New York Research Foundation.

1 0

セミナー案内
by KASHIMA Ryo 06 Sep '19

06 Sep '19

数理論理学セミナーのお知らせ東工大大岡山キャンパスで定期的に開催しているセミナー（普段はlogic-mlには流していません）の特別版を　　９月８日（金）と１５日（金）に開催します。以下に「話者（所属）題目」の一覧を載せました。どなたでも参加できますが、普段のセミナー案内を受け取っていない方の場合はご一報ください。 ----- 鹿島亮東京工業大学情報理工学院数理・計算科学系 kashima(a)is.titech.ac.jp ＝＝＝＝＝＝＝＝【８日（金）】西牟田祐樹（慶應大）一般化乗法的論理結合子のシーケント化定理とdecomposabilityについて藤原誠（早大）Bar induction and restricted classical logic 武原直紀（東工大）直観主義二階命題論理と論理式完備ハイティング代数について松田直祐（神奈川大）Curry's last problemへの弱い解答中村誠希（東工大）関係Kleene代数におけるatomic negationについて（仮題）新屋良磨（東大）論文紹介 Cyclic Arithmetic Is Equivalent to Peano Arithmetic 【１５日（金）】池上貴大（東工大）様相命題論理におけるツリーシークエント計算（仮題）河野友亮（東工大）Quantum logic の implication algebra と restricted negation について（仮題）鹿島亮（東工大）２階の関数記号を持つ１階述語論理について山﨑紗紀子（首都大）ゲーデル・マッキンゼイ・タルスキの定理の証明論的証明ー後件複数な直観主義論理のG3-style sequent calculus を用いてー大森仁（京大）Jaskowskiのdiscussive logicの周辺金沢誠（国立情報学研）Context-Free Languages with Finite Context and Kernel Properties 高橋正子 Grzegorczyk階層について＝＝＝＝以上＝＝＝＝

1 8

リマインダ: フォーマルアプローチ特集論文募集のご案内
by ken.mano.eh＠hco.ntt.co.jp 02 Sep '19

02 Sep '19

皆様， IEICE フォーマルアプローチ特集の締め切り（令和元年 9 月 24 日 (火)）が近づいてまいりました．皆さまの周辺の方に再度ご周知いただき，ご投稿をご検討されている方には，ラストスパートをよろしくお願いいたします．真野 =========================================================================== フォーマルアプローチ特集論文募集電子情報通信学会論文誌英文 ED 分冊フォーマルアプローチ特集編集委員会フォーマルアプローチ（形式手法・形式技法・形式理論）は，情報システムや組込みシステムの設計開発における信頼性向上の鍵となる重要な基盤です．これまで，設計対象のモデル化，要求分析と仕様記述，コード自動生成，テストと検証，保守と再利用などに関する技術と理論的知見を生み出してきました．近年の情報技術の進展に伴う対象領域の拡大に伴い，フォーマルアプローチは従来にも増して多様な分野で用いられるようになり，ますます発展しています．本小特集（2020 年 8 月号掲載）は，情報システムや組込みシステムの設計・運用におけるフォーマルアプローチについて，基礎理論から応用まで，幅広い研究を対象にしています．個別の対象領域に特化したケーススタディから，分野横断的な手法や理論まで，様々な方面から，フォーマルアプローチ研究に携わる若手研究者を奨励するとともに，この分野の研究が更に発展することを目指しております．奮って御投稿下さいますよう御案内申し上げます． 1. 対象分野主な対象は以下のとおりですが，これに限らず，「情報システムや組込みシステム及びそれをとりまく環境を定式化した上で，そのシステムの振舞いの解析や性質の導出を厳密に行い，設計・運用に関わる種々の問題の解決を図る」ことを目指した論文を広く募集します． - 基礎理論：システムの構造や振舞いの形式記述・検証に関する基礎理論 - 形式技法：ソフトウェア，ハードウェア，ネットワークなどのシステムに対する体系だった記述・検証技法 - 形式ツール：モデル検査器や定理証明器など，形式手法に基づくツール - 応用：情報システムや組込システム，回路系，情報セキュリティ，車載システム，人工知能・機械学習システム，マルチエージェントなどへの形式手法の適用事例 - 教育：教育事例 2. 論文の執筆と取扱い論文 (一般論文)，レター，及びサーベイ論文を募集します．投稿規程等は電子情報通信学会の英文誌の規程と同じです．以下の規程を御参照下さい． "The Information for Authors" (IEICE Transactions on Information and Systems) http://www.ieice.org/eng/shiori/mokuji_iss.html 3. 主なスケジュール論文投稿締切 2019 年 9 月 24 日 (火) 23:59 JST (厳守) 第一回判定通知予定 2019 年 11 月 22 日 (金) 初回修正締切 2020 年 1 月 17 日 (金) 最終判定通知予定 2020 年 3 月 6 日 (金) 発行予定 2020 年 8 月号 4. 投稿方法投稿に際しては，著者のうち少なくとも1名は本会会員でなければなりません．ただし招待論文に関してはこの限りではありません．必要な投稿資格を満たしていない著者からの投稿論文については，投稿を受け付けないこととなりますので御注意下さい．入会の案内はこちらを御覧下さい． http://www.ieice.org/jpn/join/index.html 本特集では，電子投稿のみを受付けます．論文を下記の web page から投稿して下さい．初期投稿時に，編集可能な論文本体 (TeX/Word)，図，著者の写真， biography も投稿する必要があります． https://review.ieice.org/regist/regist_baseinfo_e.aspx 投稿の際には以下の項目を選択してください． "Journal/Section" -> "[Special FO] Formal Approaches" 同時に WEB 上で著作権譲渡手続きができます．投稿手続きについて御不明な点がございましたら，問合先まで御連絡下さい． 5. 掲載料招待論文を含むすべての著者は，論文が採録となった場合，2020 年 4 月頃に掲載料をお支払い頂くことになります．2020 年 5 月 15 日までに支払いが完了しない場合には，採録取り消しとなります． 6. オープンアクセスオプション電子情報通信学会論文誌は，2019 年 1 月号掲載論文から，著者が通常の掲載料に加え追加料金を支払うことで，論文をオープンアクセスにできる選択肢を試行的に提供致します．オープンアクセスオプションに関する詳細は，"Information for Authors" (http://www.ieice.org/eng/shiori/mokuji_iss.html)を御参照下さい（オープンアクセスオプションは試行段階であり，予告なく変更されることがあります）． 7. 特集編集委員会委員長：真野健(NTT) 幹事：石川冬樹(情報研)，横川智教（岡山県立大）委員：青木利晃(北陸先端大)，青木善貴（日本ユニシス），來間啓伸(日立)，小林孝一(北大)，立石孝彰(日本IBM)，土屋達弘(阪大)，山口真悟(山口大) 8. 問合せ先本特集のホームページ: (和文) http://www.brl.ntt.co.jp/people/mano/fa2019/jp/ (英文) http://www.brl.ntt.co.jp/people/mano/fa2019/ 真野健 NTT コミュニケーション科学基礎研究所〒243-0198 神奈川県厚木市森の里若宮 3-1 ken.mano.eh(a)hco.ntt.co.jp =========================================================================== CALL FOR PAPERS Special Section on Formal Approaches The IEICE Transactions on Information and Systems announces a forthcoming special section on Formal Approaches to be published in August 2020. Formal methods and techniques play a key role in designing and developing highly reliable information systems and embedded systems. The last decades have seen various new techniques and profound theoretical results using formal methods in surprisingly many fields such as modeling, requirements analysis, specification, automatic generation of codes, testing, verification, and maintenance. They are rapidly extending their application domains as a result of the recent growth of information and communication technologies. The Special Section on Formal Approaches aims at stimulating research on formal approaches to information systems and embedded systems, ranging from fundamental theory to practical applications. Our emphasis is put on the cross-fertilization of related research fields and encouragement of young researchers. Topics: The major topics are listed below, but we solicit submissions in all areas of formal approaches, i.e., first to formalize information systems, embedded systems, and their environment, next to analyze their behavior and to derive their properties rigorously, and then to solve various problems in designing and managing the systems. - Theoretical foundations: all aspects of theory related to formal description and verification for structure and behavior of systems. - Formal techniques: techniques for mainly describing and analyzing systems, such as software, hardware and networks. - Formal tools: tools based on formal methods such as model checkers, theorem provers, and static and dynamic analyzers. - Applications: practical experiences of applying formal methods to information systems, embedded systems, circuits, security, AI systems, machine learning systems, multi-agent systems, automotive systems, etc. - Education: education on formal methods. Submission Instructions: The deadline for submission is Sep 24, 2019, 23:59 JST(GMT+9). Manuscripts should be carefully prepared according to the guideline in the "Information for Authors" (available at http://www.ieice.org/eng/shiori/mokuji_iss.html). The preferred length of the manuscript is 8 pages. Only electronic submission through the web page is accepted. Submit a complete paper and transfer copyright of the paper using the IEICE Web site https://review.ieice.org/regist/regist_baseinfo_e.aspx Authors should choose the [Special FO] Formal Approaches" as a "Journal/Section" on the online screen. Editorial Committee: Guest Editor-in-Chief: Ken Mano (NTT Communication Science Laboratories) Guest Editors: Fuyuki Ishikawa (National Institute of Informatics) Tomoyuki Yokogawa (Okayama Prefectural University) Guest Associate Editors: Toshiaki Aoki (JAIST) Yoshitaka Aoki (Nihon Unisys) Koichi Kobayashi (Hokkaido University) Hironobu Kuruma (Hitachi, Ltd.) Takaaki Tateishi (IBM Japan) Tatsuhiro Tsuchiya (Osaka University) Shingo Yamaguchi (Yamaguchi University) Further information may be obtained from the web page at: http://www.brl.ntt.co.jp/people/mano/fa2019/ All inquiries should be sent to the guest editor in chief: Ken Mano NTT Communication Science Laboratories 3-1 Morinosato Wakamiya Atsugi Kanagawa 243-0198 Japan E-mail: ken.mano.eh(a)hco.ntt.co.jp Important Dates: Submission Deadline: Sep 24, 2019 23:59 JST (GMT+9) [strict] First Notification: Nov 22, 2019 Revised Version Deadline: Jan 17, 2020 Final Notification: Mar 6, 2020 Important Notice. (1) At least one of the authors must be an IEICE member when the manuscript is submitted for review. For the application of IEICE membership, visit http://www.ieice.org/eng/member/OM-appli.html (2) When a paper has been accepted for publication, the authors are required to pay the page charges covering part of the cost of publication. Please carefully read the submission guideline at http://www.ieice.org/eng/shiori/mokuji_iss.html (3) Upon accepted for publication, all authors, including authors of invited papers, should pay the page charges covering partial cost of publication around April, 2020. If payment is not completed by May 15, 2020, your manuscript will be handled as rejection. (4) [Open Access Option] Papers published in January 2019 issue and following issues will be offered a trial basis option which can make the papers open access if authors pay an additional charge on top of the usual page charge. For details on open access options, please carefully refer to “The Information for Authors” (http://www.ieice.org/eng/shiori/mokuji_iss.html). Note that open access option is still in the pre-trial stage, and it may be changed without notice. ===========================================================================

1 0

SLACS2019プログラム確定のお知らせ
by Kensuke Kojima 31 Aug '19

31 Aug '19

皆様（複数のメイリングリストに送信しています。重複して受信の際はご容赦ください。） SLACS2019幹事の小島です。講演・懇親会参加へお申し込み下さった皆様、どうもありがとうございました。プログラムが以下のように決まりましたのでお知らせします。 SLACS 2019（記号論理と情報科学） https://sites.google.com/view/slacs-2019/home 日時: 2019年9月9日（月）（午後1時25分開始）から2019年9月10日（火）場所: 京都大学総合研究8号館講義室3 参加費: 無料。ただし、懇親会費は別途徴収します。 9月9日 13:25-13:30 オープニング 13:30-14:30 山形頼之（国立研究開発法人産業技術総合研究所） Recent progress of consistency proofs of equational systems inside bounded arithmetics 14:50-15:30 只木孝太郎（中部大学工学部情報工学科） A refinement of quantum teleportation and superdense coding by algorithmic randomness 15:30-15:50 石原豪人 Chaos and foundation of mathematics 16:10-16:50 福田陽介（京都大学大学院情報学研究科） Call-by-name, call-by-value, and the modal linear lambda calculus 16:50-17:30 中野浩（龍谷大学理工学部）近似様相を含む型の意味論について 18:30- 懇親会 9月10日 10:00-10:40 長谷川真人（京都大学数理解析研究所） A braided lambda calculus 10:40-11:20 塚田武志（東京大学）不動点算術とプログラム検証 13:00-13:40 南規楽（京都大学数理解析研究所）論理式をやりとりするプロセス代数 13:40-14:20 村井涼（北海道大学大学院）分散知識オペレータを持つ多エージェント様相論理のシークエント計算 14:40-15:20 鴨浩靖（奈良女子大学） Prologによるビルドツールの使い心地 15:20-16:00 谷口雅弥（北陸先端科学技術大学院大学） Subjunctive Markers in Intentional Logic

1 0

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml