Kisoron-ml September 2014

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

5 participants
5 discussions

JAIST Logic Seminar Series (18th Sep. 2014: Tadeusz Litak on Relational lattices)
by Katsuhiko Sano 22 Sep '14

22 Sep '14

皆様、 FAU Erlangen-Nürnberg の Tadeusz Litak さんの講演のお知らせです。ふるってご参加ください。問い合わせ先：佐野勝彦北陸先端科学技術大学院大学情報科学研究科 e-mail: v-sano(a)jaist.ac.jp ---------------------------------------------------------------------------------------------------- * JAIST Logic Seminar Series * Date: Thursday, 18th September, 2014, 15:10-17:00 Place: JAIST Collaboration Room 6 (I57-g) (Access:http://www.jaist.ac.jp/english/location/access.html) Speaker: Tadeusz Litak (Department Informatik, Technische Fakultät, FAU Erlangen-Nürnberg, Germany) Title: Relational lattices Abstract: We study an interpretation of lattice connectives as natural join and inner union between database relations with non-uniform headers. We show that this interpretation proposed by database experts (Vadim Tropashko from Oracle) yields a class of lattices which has not been considered in the existing lattice-theoretical literature. We discuss axiomatizability and decidability of their (quasi-)equational theory and propose an equational axiomatization for a corresponding abstract algebraic class. It turns out that addition of just the “header constant” to the lattice signature already allows mimicking the Maddux technique for cylindric algebras and encode the word problem for semigroups in the quasiequational theory. Relational lattices, however, are not as intangible as one may fear: for example, they do form a pseudoelementary class. We also apply the tools of Formal Concept Analysis and investigate standard contexts of relational lattices, obtaining, e.g., results on their subdirect irreducibility. This is a joint work with Szabolcs Mikulas and Jan Hidders ----------------------------------------------------------------------------------------------------

2 2

再送：数学基礎論若手の会
by YOSHIDA Satoru 22 Sep '14

22 Sep '14

皆様重複して受け取られた場合はご容赦ください。数学基礎論若手の会2014のご案内です。数学基礎論を専攻する学生および若手研究者の研究交流を目的とする合宿形式の研究集会です．講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しております．また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します．多くの方々のご参加およびご講演をお待ちしています．日程：11月19日（水）午後－21日（金）午前場所：鳥取市サイクリングターミナル砂丘の家（鳥取砂丘付近） http://www.city.tottori.lg.jp/www/contents/1198114185831/ 幹事：吉田聡（鳥取環境大学） satoru-y(a)kankyo-u.ac.jp ホームページ： http://misc.kankyo-u.ac.jp/~satoru-y/wakate14/ 今年度若手の会申込み要領については上記ホームページをご参照ください。 -- 吉田聡<YOSHIDA, Satoru> 鳥取環境大学

1 0

Prof. Aleksy Schubert at NII Logic Seminar
by Makoto Tatsuta 22 Sep '14

22 Sep '14

Prof. Aleksy Schubert at NII Logic Seminar Date: September 26, 2014, 14:00--16:00 Place: National Institute of Informatics, Room 1716 (17th floor) 場所: 国立情報学研究所 17階 1716室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Aleksy Schubert (University of Warsaw) (1) Title: Undecidability and complexity in fragments of first-order intuitionistic logic Abstract: In case of classical first-order logic there is a full characterisation of decidable and undecidable classes of formulae depending on the quantifier prefix and the vocabulary that is used. First-order logic in intuitionistic case lacks this kind of classification since there is no prefix normal form and actually the prenex fragment of the logic is in many cases much weaker than the general calculus. However, there is one meaningful stratification of the intuitionistic logic similar to the prenex form. We can consider classes of formulae that would result in a particular prefix of quantifiers when transformed using classical equivalences. The status of decidable and undecidable cases within this stratification will be presented as well as the complexity of known subcases. (2) Title: Verification of programs using Frama-C and Why3 Abstract: Frama-C is a tool that makes it possible to do a variety of analyses for C programs annotated with C specification language called ACSL (The ANSI/ISO C Specification Langage). One of the possible ways to use Frama-C is to generate verification conditions for appropriately defined Hoare logic that is in line with C programming language semantics. These verification conditions can subsequently be discharged by Why3 tool that makes it possible to manage the proving of necessary properties. During the talk I will present an overview of the tools and show a number of interesting examples to demonstrate how these tools work together to make possible verification of practical programs. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内
by Yoshihito Tanaka 22 Sep '14

22 Sep '14

九州大学マス・フォア・インダストリ研究所の溝口先生の代理で投稿いたします． ========================================================================= 研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内　　　　　　　　　　　　　　　　　　　(English version is below.) 12月3日(水)-5日(金)に九州大学西新プラザにて, 研究集会「高信頼な理論と実装のための定理証明および定理証明器」を開催します. 皆様のご参加をお待ちしています. 日時：2014年 12月3日(水) 〜 12月5日(金) 場所：九州大学・西新プラザ (福岡市早良区西新2-16-23) http://bit.ly/QdaiNishijin 福岡空港から地下鉄で西新駅まで約20分, その後, 徒歩約10分. プログラム：詳細は未定(準備中)です. みなさまのご講演をお待ちしています. Adam Chlipala氏 (MIT, USA), Cyril Cohen 氏 (Univ. Gothenburg, Sweden) をお招きして, Coqおよび Ssreflect, MathCompに関する御講演を頂く予定です. 参加者と講演の数を大体把握しておきたいと思いますので，参加される方は 10月半ばまでに下の参加申し込みを下記メールアドレスまでお送りください．参加者には，できるだけ講演していただければと思います．申込み・問い合わせ先: tpp2014(a)imi.kyushu-u.ac.jp (溝口佳寛(九州大学)) URL: http://coop-math.ism.ac.jp/event/2014E04 (注. 作成途中です.「TPP2014 数学」で検索してみて下さい.) ------------------------------------------------------------------------- TPP 2014 参加申し込みお名前：ご所属：講演　：する／しない懇親会：参加する／参加しない講演する場合タイトル：（講演のタイトルが決まっていなければ，TBAでもかまいません．決まったらご連絡ください．）講演希望日: (○/×) 12/3 (○/×) 12/4 (○/×) 12/5 その他(ご意見/ご要望ありましたらお願いします): ------------------------------------------------------------------------- ========================================================================= Workshop: Theorem proving and provers for reliable theory and implementations (TPP2014) This is the call for participation for TPP2014, to be held on Dec. 3(Wed) - 5(Fri), 2014 at Kyushu University. Date: 2014/12/03 around 1pm to 12/05 around 3pm Venue: Nishijin Plaza, Kyushu University (2-16-23 Nishijin, Sawara-ku, Fukuoka City) http://bit.ly/QdaiNishijinPDF Invited Speakers: Adam Chlipala (MIT, USA) Cyril Cohen (Univ. Gothenburg, Sweden) If you are planning to attend the meeting, please send the information slip below to the indicated address by mid-October. Submission/questions to: 　　　tpp2014(a)imi.kyushu-u.ac.jp (Yoshihiro Mizoguchi) URL: http://coop-math.ism.ac.jp/event/2014E04 (Tentative Japanese HP. Revised English HP will be notified later.) ------------------------------------------------------------------------- TPP 2014 Registration Name: Affiliation: Will give a talk: Yes/No Will attend the party: Yes/No Title of the talk: (If it is not decided yet, TBA is OK.) Which date do you prefer to talk ? 12/3 (OK/NG) 12/4 (OK/NG) 12/5 (OK/NG) Requests for the organizer (if any): ------------------------------------------------------------------------- =========================================================================

1 0

Prof. Aart Middeldorp at NII Logic Seminar
by Makoto Tatsuta 17 Sep '14

17 Sep '14

Prof. Aart Middeldorp at NII Logic Seminar Date: September 22, 2014, 14:00--16:00 Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Aart Middeldorp (University of Innsbruck) Title: Proving AC Termination by Knuth-Bendix Orders Abstract: Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-founded orders that are compatible with the AC axioms. In this talk we consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is enhanced to a more powerful AC-compatible order and we modify the latter to amend its lack of monotonicity on non-ground terms. We present new complexity results and compare the various orders on problems in termination and completion. The talk is based on joint work with Nao Hirokawa, Sarah Winkler, and Akihisa Yamada. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Kisoron-ml September 2014