Logic-ml August 2017

11 participants
12 discussions

セミナー案内
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

FINAL CALL FOR PAPERS: Logic and Engineering of Natural Language Semantics 14 (LENLS 14), Deadline Extended
by Katsuhiko Sano 31 Aug '17

31 Aug '17

[Apologies for multiple copies] ================================================================= FINAL CALL FOR PAPERS **Deadline extended to September 7, 2017** Logic and Engineering of Natural Language Semantics 14 (LENLS 14) Workshop Site : Bunkyo School Building in University of Tsukuba, Tokyo Campus Bunkyo-ku, Tokyo, Japan http://www.tsukuba.ac.jp/en/access/tokyocampus-access Dates : November 13-15, 2017 Contact Person: Katsuhiko Sano (Hokkaido University) Contact Email : lenls14[[at]]easychair.org Website : http://www.is.ocha.ac.jp/~bekki/lenls/ ================================================================= Chair: Katsuhiko Sano (Hokkaido University) Co-chair: Eric McCready (Aoyama Gakuin University) Daisuke Bekki (Ochanomizu University/JST CREST) Koji Mineshima (Ochanomizu University/JST CREST) Invited Speakers: - Craige Roberts (The Ohio State University) - Ivano Ciardelli (University of Amsterdam) - Shoichi Takahashi (Aoyama Gakuin University) LENLS is an annual international workshop on formal syntax, semantics and pragmatics. It will be held as one of the workshops of the JSAI International Symposia on AI (isAI2017) (https://www.ai-gakkai.or.jp/isai/) sponsored by the Japan Society for Artificial Intelligence (JSAI). Aims and Topics: ================ We invite submissions to this year's workshop on topics in formal syntax, semantics and pragmatics, and related fields, including but in no way limited to the following: - Formal syntax, semantics and pragmatics of natural language - Model-theoretic and/or proof-theoretic semantics of natural language - Computational Semantics - Game-theoretic/Bayesian approaches to pragmatics - Nonclassical Logic and its relation to natural language (especially Substructural/Fuzzy/Categorical/Topological logics) - Formal Philosophy of language - Scientific methodology and/or experimental design for linguistics Submissions: ============ Abstracts (anonymous, up to 4 pages, including figures and references, A4 size, with 12 point font) must be submitted electronically in PDF format at: https://easychair.org/conferences/?conf=lenls14 When the abstract is accepted, the author is expected to submit a full paper (10-14 pages) before the workshop. The online proceedings of the workshop will be available at the conference site. Important dates: ================ Abstract submission deadline: September 7, 2017 (extended) Notification of acceptance: September 30, 2017 Deadline for camera-ready copy: mid-October, 2017 LENLS14: November 13-15, 2017 Sponsor: ======== LENLS is being organized by an alliance of "Establishment of Knowledge-Intensive Structural Natural Language Processing and Construction of Knowledge Infrastructure" (http://nlp.ist.i.kyoto-u.ac.jp/CREST/?en) project, funded by JST CREST Programs "Advanced Core Technologies for Big Data Integration" (http://www.jst.go.jp/kisoken/crest/en/research_area/ongoing/areah25-6.html). Workshop Organizers/Program Committee: ====================================== - Katsuhiko Sano (Hokkaido University) - Eric McCready (Aoyama Gakuin University) - Daisuke Bekki (Ochanomizu University/JST CREST) - Koji Mineshima (Ochanomizu University/JST CREST) - Alastair Butler (National Institute for Japanese Language and Linguistics) - Richard Dietz (iCLA, Yamanashi Gakuin University) - Naoya Fujikawa (Tokyo Metropolitan University) - Yoshiki Mori (University of Tokyo) - Yasuo Nakayama (Osaka University) - David Y. Oshima (Nagoya University) - Osamu Sawada (Mie University) - Wataru Uegaki (Leiden University) - Katsuhiko Yabushita (Naruto University of Education) - Tomoyuki Yamada (Hokkaido University) - Shunsuke Yatabe (Kyoto University) - Kei Yoshimoto (Tohoku University)

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 30 Aug '17

30 Aug '17

皆様スワンジー大学のArnold Beckmann先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学系 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * The seminar below is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, EU FP7 Marie Curie Actions IRSES project CORCON. (http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/), and EU Horizon 2020 Marie Skłodowska-Curie actions RISE project CID. Date: Friday 15, September, 2017, 15:20-17:00 Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Professor Arnold Beckmann (University of Swansea, Head of Department of Computer Science) http://www.cs.swan.ac.uk/~csarnold/ Title: Provably Total NP Search Problems of Bounded Arithmetic and beyond Abstract: Bounded Arithmetic forms a collection of weak theories of Arithmetic related to complexity classes of functions like the Polynomial Time Hierarchy. Many connections between Bounded Arithmetic and important questions about complexity classes have already been established. Recent research considers total NP search problems in the context of Bounded Arithmetic. Total NP search problems have been studied by Papadimitriou et al as a means to characterise the complexity of natural search problems which cannot be analysed as decision problems. In my talk I will review the research programme of characterising the provably total NP search problems in Bounded Arithmetic, and explain why it is important for current research questions in the area. I will describe recent results about the provably total NP search problems of a Bounded Arithmetic theories related to PSPACE and EXPTIME reasoning. I will also describe this program for theories beyond Bounded Arithmetic like Peano arithmetic, and what impact this might have on Complexity Theory.

1 0

3rd CALL FOR PAPERS: Logic and Engineering of Natural Language Semantics 14 (LENLS 14)
by Katsuhiko Sano 26 Aug '17

26 Aug '17

[Apologies for multiple copies] ================================================================= 3rd CALL FOR PAPERS Logic and Engineering of Natural Language Semantics 14 (LENLS 14) Workshop Site : Bunkyo School Building in University of Tsukuba, Tokyo Campus Bunkyo-ku, Tokyo, Japan http://www.tsukuba.ac.jp/en/access/tokyocampus-access Dates : November 13-15, 2017 Contact Person: Katsuhiko Sano (Hokkaido University) Contact Email : lenls14[[at]]easychair.org Website : http://www.is.ocha.ac.jp/~bekki/lenls/ ================================================================= Chair: Katsuhiko Sano (Hokkaido University) Co-chair: Eric McCready (Aoyama Gakuin University) Daisuke Bekki (Ochanomizu University/JST CREST) Koji Mineshima (Ochanomizu University/JST CREST) Invited Speakers: - Craige Roberts (The Ohio State University) - Ivano Ciardelli (University of Amsterdam) - Shoichi Takahashi (Aoyama Gakuin University) LENLS is an annual international workshop on formal syntax, semantics and pragmatics. It will be held as one of the workshops of the JSAI International Symposia on AI (isAI2017) (https://www.ai-gakkai.or.jp/isai/) sponsored by the Japan Society for Artificial Intelligence (JSAI). Aims and Topics: ================ We invite submissions to this year's workshop on topics in formal syntax, semantics and pragmatics, and related fields, including but in no way limited to the following: - Formal syntax, semantics and pragmatics of natural language - Model-theoretic and/or proof-theoretic semantics of natural language - Computational Semantics - Game-theoretic/Bayesian approaches to pragmatics - Nonclassical Logic and its relation to natural language (especially Substructural/Fuzzy/Categorical/Topological logics) - Formal Philosophy of language - Scientific methodology and/or experimental design for linguistics Submissions: ============ Abstracts (anonymous, up to 4 pages, including figures and references, A4 size, with 12 point font) must be submitted electronically in PDF format at: https://easychair.org/conferences/?conf=lenls14 When the abstract is accepted, the author is expected to submit a full paper (10-14 pages) before the workshop. The online proceedings of the workshop will be available at the conference site. Important dates: ================ Abstract submission deadline: August 31, 2017 Notification of acceptance: September 30, 2017 Deadline for camera-ready copy: mid-October, 2017 LENLS14: November 13-15, 2017 Sponsor: ======== LENLS is being organized by an alliance of "Establishment of Knowledge-Intensive Structural Natural Language Processing and Construction of Knowledge Infrastructure" (http://nlp.ist.i.kyoto-u.ac.jp/CREST/?en) project, funded by JST CREST Programs "Advanced Core Technologies for Big Data Integration" (http://www.jst.go.jp/kisoken/crest/en/research_area/ongoing/areah25-6.html). Workshop Organizers/Program Committee: ====================================== - Katsuhiko Sano (Hokkaido University) - Eric McCready (Aoyama Gakuin University) - Daisuke Bekki (Ochanomizu University/JST CREST) - Koji Mineshima (Ochanomizu University/JST CREST) - Alastair Butler (National Institute for Japanese Language and Linguistics) - Richard Dietz (iCLA, Yamanashi Gakuin University) - Naoya Fujikawa (Tokyo Metropolitan University) - Yoshiki Mori (University of Tokyo) - Yasuo Nakayama (Osaka University) - David Y. Oshima (Nagoya University) - Osamu Sawada (Mie University) - Wataru Uegaki (Leiden University) - Katsuhiko Yabushita (Naruto University of Education) - Tomoyuki Yamada (Hokkaido University) - Shunsuke Yatabe (Kyoto University) - Kei Yoshimoto (Tohoku University)

1 0

[Deadline Extension] JURISIN2017: call for Papers
by Ken Satoh (web mail) 22 Aug '17

22 Aug '17

CFP: Eleventh International Workshop on Juris-informatics (JURISIN 2017) homepage: http://research.nii.ac.jp/~ksatoh/jurisin2017 **************************************************** The submission deadline is extended to 6 September. **************************************************** ** Workshop dates November 14 - 15, 2017 ** Venue Tokyo Campus, University of Tsukuba, Tokyo, Japan http://www.tsukuba.ac.jp/en/access/tokyocampus-access ** Important Dates Submission Deadline: September 6, 2017 Notification: October 6, 2017 Camera-ready due: October 13, 2017 ** Aims and Scope Juris-informatics is a new research area which studies legal issues from the perspective of informatics. The purpose of this workshop is to discuss both the fundamental and practical issues among people from the various backgrounds such as law, social science, information and intelligent technology, logic and philosophy, including the conventional "AI and law" area. We solicit unpublished papers on theories, technologies and applications on juris-informatics. ** Relevant topics include, but are not limited to, the following: Model of legal reasoning Argumentation / Negotiation / Argumentation agent Legal term ontology Formal legal knowledge-base / Intelligent management of legal knowledge-base Translation of legal documents Information retrieval of legal texts Computer-aided law education Use of Informatics and AI in law Legal issues on applications of robotics and AI to society Social implications of use of informatics and AI in law Natural language processing for legal knowledge Verification and validation of legal knowledge systems Any theories and technologies which is not directly related with juris-informatics but has a potential to contribute to this domain ** Invited Speakers Kevin D. Ashley (University of Pittsburgh) Katsumi Nitta (Tokyo Institute of Technology) ** Submissions We welcome and encourage the submission of high quality, original papers, which are not simultaneously submitted for publication elsewhere except as a submission to JURIX 2017 (The 28th International Conference on Legal Knowledge and Information Systems). The double submission policy with JURIX 2017 is as follows: Papers being submitted both to JURISIN2017 and JURIX2017 must note this on the title page. A paper to be presented at JURISIN2017 must be withdrawn from JURIX2017 and vice versa according to the choice by the authors. If the authors do not follow this double submission policy, the paper by the authors will not be included in the proceedings of JURISIN 2017. Papers should be written in English, formatted according to the Springer Verlag LNCS style in a pdf form, which can be obtained from http://www.springeronline.com and not exceed 14 pages including figures, references, etc. If you use a word file, please follow the instruction of the format, and then convert it into a pdf form and submit it at the paper submission page. If a paper is accepted, at least one author of the paper must register the workshop and present it. We strongly encourage an online registration. You can submit your paper at "https://easychair.org/conferences/?conf=jurisin2017". If you cannot submit a paper by EasyChair System by some trouble, please send email to "ksatoh[at]nii.ac.jp" ** Post Proceedings Selected papers will be published as a post-proceedings via Springer Verlag LNAI series after the second round of review after the workshop. ** Workshop Chair Ken Satoh, National Institute of Informatics and Sokendai, Japan ** Steering Committee Members Takehiko Kasahara, Toin Yokohama University Makoto Nakamura, Nagoya University, Japan Katsumi Nitta, Tokyo Institute of Technology, Japan Seiichiro Sakurai, Meiji Gakuin University, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Satoshi Tojo, JAIST, Japan Katsuhiko Toyama, Nagoya University, Japan ** Advisory Committee Members Trevor Bench-Capon, The University of Liverpool, UK Tomas Gordon, Fraunfoher FOKUS, Germany Henry Prakken, University of Utrecht & Groningen, The Netherlands John Zeleznikow, Victoria University, Australia Robert Kowalski, Imperial College London, UK Kevin Ashley, University of Pittsburgh, USA ** Program Committee Members Thomas Agotnes, University of Bergen, Norway Ryuta Arisaka, National Institute of Informatics, Japan Kristijonas Cyras Imperial College London Marina De Vos, University of Bath, UK Phan Minh Dung, AIT, Thailand Randy Goebel, University of Alberta, Canada Guido Governatori, Data61, Australia Tatsuhiko Inatani, Kyoto University, Japan Tokuyasu Kakuta, Nagoya University, Japan Yoshinobu Kano, Shizuoka University, Japan Mi-Young Kim, University of Alberta, Canada Nguyen Le Minh, JAIST, Japan Beishui Liao, Zhejiang University, Chaina Hatsuru Morita, Tohoku University, Japan Makoto Nakamura, Nagoya University, Japan Yoshiaki Nishigai, Nihon University, Japan Konatsu Nishigai, Tokyo Metropolitan University, Japan Katsumi Nitta, Titech, Japan Paulo Novais, University of Minho, Portugal Julian Padget, University of Bath, UK Ginevra Peruginelli, ITTIG-CNR, Italy Katsuhiko Sano, Hokkaido University, Japan Giovanni Sartor, EUI/CIRSFID, Italy Seiichiro Sakurai, Meiji Gakuin University, Japan Ken Satoh, National Institute of Informatics and Sokendai Akira Shimazu, JAIST, Japan Fumio Shimpo, Keio University, Japan Satoshi Tojo, JAIST, Japan Katsuhiko Toyama, Nagoya University, Japan Rob van den Hoven van Genderen, VU University Amsterdam, The Netherlands Leon van der Torre, University of Luxembourg, Luxembourg Bart Verheij, University of Groningen, The Netherlands Katsumasa Yoshikawa, IBM Research Tokyo, Japan Masaharu Yoshioka, Hokkaido University, Japan Harumichi Yuasa, Institute of Information Security, Japan Yueh-Hsuan Weng, Tohoku University, Japan Adam Wyner, University of Aberdeen, UK For any inquiry concerning the workshop, please send it to "ksatoh[at]nii.ac.jp"

1 0

名古屋ロジックセミナー (Linda Brown Westrick氏の講演 8/24)
by Takayuki Kihara 16 Aug '17

16 Aug '17

皆様，名古屋大学の木原貴行です．この度，コネチカット大学の Linda Brown Westrick 氏の名古屋訪問の折に，下記の要領で名古屋ロジックセミナーを開催することとなりました．多数のご参加をお待ちしております．名古屋ロジックセミナー http://www.math.mi.i.nagoya-u.ac.jp/~kihara/logic-seminar.html 日時：8月24日 (木) 15:30〜場所：名古屋大学大学院情報学研究科棟 314室講演者：Linda Brown Westrick (コネチカット大学) 題目 Uncountable free abelian groups via admissible computability 概要 One way to study structures of uncountable cardinality κ is to generalize the notion of computation. Saying that a subset of κ is κ-c.e. if it is Σ^0_1 definable (with parameters, in the language of set theory) over L_κ provides the notion of κ-computability. We may also quantify over subsets of L_κ, providing a notion of a κ-analytic set (here we assume V=L). In this setting, we consider the difficulty of recognizing free groups and the complexity of their bases. For example, if κ is a successor cardinal, the set of free abelian groups of size κ is Σ^1_1-complete. The resolution of questions of this type is more complex for other κ, and a few questions remain open. This is joint work with Greenberg and Turetsky. -------- Takayuki Kihara Graduate School of Informatics, Nagoya University, Japan URL: http://math.mi.i.nagoya-u.ac.jp/~kihara/ Email: kihara(a)i.nagoya-u.ac.jp

1 0

第二十八回 ALGI（代数，論理，幾何と情報科学研究集会）の暫定プログラムと懇親会参加について
by 西澤弘毅 11 Aug '17

11 Aug '17

logic-mlメーリングリストの皆様，神奈川大学の西澤弘毅と申します。第二十八回 ALGI（代数，論理，幾何と情報科学研究集会）の暫定プログラムのアナウンスをさせていただきます。 < 重複してお受け取りの節はご容赦願います。> ご参加をお待ちしております。 --------------------------------------------------------------------- **************************************************************** * 第二十八回 ALGI（代数，論理，幾何と情報科学研究集会） * * * * 2017年8月28日（月）午後～8月29日（火） * * 鹿児島大学郡元キャンパス理学部 1号館 101講義室 * * * * 暫定プログラムのお知らせと講演募集 * **************************************************************** ALGI (Algebra, Logic, Geometry and Informatics) は、代数学や論理学、幾何学の情報科学への応用について、および情報科学の代数学や論理学、幾何学への応用についての研究集会で、年一回の頻度で開催されています。今年からウェブサイトがこちらに移動しました。 https://sites.google.com/site/algimeeting/home 第二十八回 ALGI の開催場所や暫定プログラムはこちらで確認できます。会場の手配は鹿児島大学の古澤仁先生にお願いしています。 https://sites.google.com/site/algimeeting/home/28 講演枠が５つ空いております。講演を希望される方は、・題目・講演者名・e-mail address ・所属・梗概・希望時間・講演に必要な道具などの情報を西澤（nishizawa AT kanagawa-u.ac.jp）までお寄せください。また、一日目の夕方に鹿児島大学周辺で懇親会を予定しておりますので、懇親会への参加を希望される方は、8/23（水）までに上記アドレスにメールでお知らせください。 ALGI 自体は申し込み不要で自由にご参加いただけます。できるだけ多くの皆さんのご講演・ご参加をお待ちしております。なお、以前お知らせしたメーリングリストの移行については、混乱を避けるため第二十八回 ALGI の開催後に行います。その際はご協力よろしくお願いいたします。西澤弘毅（神奈川大学）津曲紀宏（崇城大学） -- 西澤弘毅神奈川大学工学部情報システム創成学科〒221-8686 神奈川県横浜市神奈川区六角橋3-27-1 nishizawa(a)kanagawa-u.ac.jp TEL（代表）045-481-5661 （内線：3378）

1 0

【論文募集】「コンピュータソフトウェア」サーベイ論文特集【〆切 9/30】
by Kazutaka Matsuda 10 Aug '17

10 Aug '17

（複数のメーリングリストに投稿しております．重複して受けとられましたらご容赦ください）皆様，東北大学の松田です．日本ソフトウェア科学会誌「コンピュータソフトウェア」では，サーベイ論文特集を企画しており，下記の要領で論文を募集（9/30 〆切）しております．どうぞ，投稿をご検討いただければ幸いです． ============================================================== 日本ソフトウェア科学会誌「コンピュータソフトウェア」「サーベイ論文」特集論文募集 http://www.jssst.or.jp/edit_news/detail/id=280 日本ソフトウェア科学会の学会誌「コンピュータソフトウェア」の使命の一つは，ソフトウェア科学・技術のすぐれた解説を通じた知識の普及および学術の発展への貢献です．本誌では折に触れ解説論文を掲載していますが，より多様なテーマに関する独特な視点からの興味深い分析を広く共有すべく，独自の切り口での網羅的な文献調査に基づく解説を「サーベイ論文」として募集します．サーベイ論文といえば，大きなテーマに対して，深い知識だけでなく，広く網羅的な知識が要求され，各分野で名の通った専門家が執筆するものというイメージがあるかもしれません．本学会誌のサーベイ論文では，このようなイメージとは一線を画した，掘り下げ方や解説の切り口などに新しい視点を与える，特定のテーマに関する網羅的なサーベイを期待しています．例えば，一つの研究を完成させる過程でその新規性および有用性を裏付けるために挙げるべき関連研究に対し，独自の観点や関連付けを与えて整理することができるでしょう．「サーベイ論文特集」は，このサーベイ論文の方向性を示し，一般投稿論文として定着させることを目的にしています．2012年2月号の第1回特集以来，年に一度のペースで特集を企画しており，今回は第7回目となります．今回も引き続き，各研究の周辺にテーマを適切に設定し，その範囲の文献を深い理解とともに網羅的に解説するというサーベイ論文の趣旨を広く周知し，さらに採択数を増やしていきたいと考えています．多くのご投稿をお待ちしております．博士論文等を執筆する過程で調査した文献の解説も広く歓迎します． [対象分野] コンピュータソフトウェアがカバーするすべての分野，例えば以下の技術や分野に関わるもの：アルゴリズム，プログラミング言語と処理系，数値的・記号的計算，システムソフトウェア，高信頼ソフトウェア，データベース，データマイニング，人工知能，ロボティクス，人間－計算機インタラクション，コンピュータネットワークをはじめとするソフトウェア科学・工学の分野において，新しい視点を与える文献の解説．オリジナルの結果を含むかどうかは問いません． [執筆要領] 日本ソフトウェア科学会誌「コンピュータソフトウェア」の関連諸規定をご参照の上，投稿論文のPDFファイルと「投稿メモ」を jssst-survey2018_at_se.cs.titech.ac.jp （_at_を@で置き換えて下さい）宛てにお送りください．学会誌関連諸規定は以下でご参照いただけます． http://www.jssst.or.jp/edit/kitei/ [スケジュール] 論文投稿締切り：2017年9月30日 17:00 特集号刊行予定：2018年8月号（査読プロセスの進行状況により掲載予定号に間に合わない場合があります．その場合でも特集論文として扱われます．） [特集号編集委員] 川端英之（広島市立大学），林晋平（東京工業大学），松田一孝（東北大学），松野裕（日本大学），櫻田英樹（NTT） [問合せ先] jssst-survey2018_at_se.cs.titech.ac.jp （_at_を@で置き換えて下さい）

1 0

PPLサマースクール2017: 参加募集
by Takahito Aoto 07 Aug '17

07 Aug '17

PPLサマースクール2017のご案内です． (重複して受信された場合はご容赦願います．) PPLサマースクールは，日本ソフトウェア科学会・プログラミング論研究会主催のイベントです．今回も，例年と同様に日本ソフトウェア科学会大会の併設企画として開催いたします．今回のテーマは「Isabelle/HOL による証明とプログラミング」で，講師はインスブルック大学の山田晃久様にお願いしております．参加申し込み方法などを含む詳細につきましては， http://ppl.jssst.or.jp/?ss2017 をご覧ください．是非ご参加をご検討いただければ幸いです． --- 青戸等人(新潟大学) ------------------------------------------------------------------------ PPLサマースクール2017 Isabelle/HOL による証明とプログラミング日本ソフトウェア科学会 (JSSST) プログラミング論研究会 (PPL) 主催日本ソフトウェア科学会第34回大会併設企画 Webページ: http://ppl.jssst.or.jp/?ss2017 講師：山田晃久(インスブルック大学) 2017年 9月 18日 (月) 10:00 - 17:00 慶應義塾大学日吉キャンパス == 概要 == Isabelle/HOL は，1986年に Lawrence Paulson によって創始され，現在はミュンヘン工科大学 Tobias Nipkow のチームを中心にメンテナンスされている証明支援ツールです． Isabelle/HOL の特徴は，スマートな証明環境 (jEdit)，強力な自動証明のサポート (Sledgehammer)，Haskell 等への自然なコード輸出 (code export)，多彩でオープンなライブラリ (Archive of Formal Proofs; AFP) などが挙げられます．本セミナーでは，Isabelle/HOL を用いた定理証明と，正しさの保証されたプログラム開発方法を，実践を通して紹介します．また AFP より，代数的数計算ライブラリなど，そのごく一部を紹介します． Isabelle には歴史的経緯からさまざまなクセがあり，学習を困難にしている要因となっていると考えられますが，本セミナーでは証明言語 Isar による，クセを排した“行儀のよい”証明の書き方に徹します．実習形式で行いますので，受講に際してはノートパソコンをご持参ください．なお，Isabelle/HOL をストレスなく利用するために，ある程度高性能なノートパソコンを推奨します．受講にあたっては，簡単な証明を書ける程度の基本的な論理学の知識を習得していること，また関数型言語の利用経験があることが推奨されます． == 講師紹介 == 山田晃久 (やまだあきひさ) http://cl-informatik.uibk.ac.at/users/ayamada/ インスブルック大学ポスドク．項書き換え系の停止性証明法に関する研究で， 2014年名古屋大学情報科学研究科博士課程を修了．同年，産業技術総合研究所にて組み合わせテストツール Calot の開発に従事．2015年より，インスブルック大学にて項書換え系，プログラム解析技法などの形式証明ライブラリ IsaFoR の開発プロジェクトに参加．情報処理学会正会員． == 参加費・参加申し込み == PPLサマースクールの参加費は以下の通りです．学生会員1000円, 学生非会員2000円, 一般会員2000円, 一般非会員3000円参加ご希望の方は，日本ソフトウェア科学会第34回大会共通の参加登録ページ https://jssst2017.wordpress.com/%e5%8f%82%e5%8a%a0%e7%94%b3%e3%81%97%e8%be%… から，お申し込みください．事前登録をお願いしております． == 問い合わせ先 == PPLサマースクール2017 幹事青戸等人 (新潟大学) E-mail: aoto(a)ie.niigata-u.ac.jp ------------------------------------------------------------------------

1 0

SLACS2017プログラム確定のお知らせと懇親会追加募集
by 安部達也 04 Aug '17

04 Aug '17

皆様（複数のメイリングリストに送信しています。重複して受信の際はご容赦ください。） SLACS2017幹事、千葉工大の安部です。講演・懇親会参加へお申し込みいただいた方々、ありがとうございました。今回は、以下のご案内をさせていただきます。 1. プログラムが確定しましたのでお知らせします。 2. 懇親会の参加について追加募集（若干名）を行います。 SLACS2017（記号論理と情報科学） http://super.para.media.kyoto-u.ac.jp/~abet/slacs2017/ 日時 2017年8月8日（火）から2017年8月9日（水）（前日まで数学基礎論サマースクールが明治大学で行われています。）場所千葉県習志野市津田沼2-17-1 千葉工業大学津田沼キャンパス 6号館3階633室参加費無料。ただし、懇親会費（3000から5000円程度）は別途徴収します。 1. プログラム（敬称略）は以下のとおり決定しました。 8月8日（火）オープニング 13:25–13:30 セッション1：座長未定 13:30–14:05 山形頼之（産総研） Validity of bilateral classical logic and its application 14:05–14:40 武原直紀（東工大）論理式完備ハイティング代数による直観主義二階命題論理のカット除去定理についてセッション2：座長未定 15:00–15:35 伴睦久（東京大） Self-identification on Social Software 15:35–16:10 福田陽介（京都大）準複数結論自然演繹による爆発則の再定式化セッション3：座長未定 16:30–17:05 内藏理史（東京大）再帰的な確率的プログラムの実行時間の二次のモーメントのための述語変換子 17:05–17:40 西脇友一（東京大） Contextual Modality through Iterated Enrichment 懇親会 18:00–20:00 福盛園（JR津田沼駅近く）SLACS2017のウェブページに地図を載せています 8月9日（水）セッション4：座長未定 10:00–10:35 酒井千尋（奈良女子大） TBA 10:35–11:10 上村太一（京都大） TBA セッション5：座長未定 11:30–12:05 木村大輔（東邦大） TBA 12:05–12:40 中澤巧爾（名古屋大） TBA クロージング 12:40–12:45 2. 懇親会会場を決定しました。当日飛び入りは不可能とのことですが、事前に連絡しておけば（会場の広さの都合上）若干名であれば対応可能とのことですので、追加募集いたします。参加を希望される方は幹事までご連絡ください。先着順に受け付けますのでご希望にそえないこともありますがご了承ください。

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml August 2017