タグ別アーカイブ: seminar

The 18th Logic and Computation Seminar

Date: Friday,  15 November 2019, 13:30-18:00
Place:  Nishijin Plaza, Multi-purpse Room(2-16-23 Nishijin, Sawara-ku, Fukuoka-shi)

13:30 – 14:10 Daniel Gaina (Kyushu University, Japan)
Birkhoff Completeness for Hybrid-Dynamic First-Order Logic
14:30 – 15:00 Walter Guttmann(JSPS International Research Fellow /
University of Canterbury, New Zealand)
Algebras for Minimum Spanning Tree Problems
15:20 – 15:50 Hitoshi Furusawa (Kagoshima University, Japan)
On Continuity of Relations
16:10 – 16:40 Yasuo Kawahara (Kyushu University, Japan)
History of Relational Calculus
17:00 –  18:00 Free Discussion

Contact: Yoshihiro Mizoguchi (Kyushu University)
ym @ imi.kyushu-u.ac.jp

日時: 2019年11月15日(金) 13:30-18:00
場所: 九州大学西新プラザ多目的室 (福岡市早良区西新2-16-23)

13:30 – 14:10 Daniel Gaina (九州大学)
演題: Birkhoff Completeness for Hybrid-Dynamic First-Order Logic
概要: Hybrid-dynamic first-order logic is a kind of modal logic obtained by enriching many-sorted first-order logic with features that are common to hybrid and to dynamic logics. This provides us with a logical system with an increased expressive power thanks to a number of distinctive attributes:
(a) first, the possible worlds of Kripke structures, as well as the nominals used to identify them, are endowed with an algebraic structure;
(b) second, we distinguish between rigid symbols, which have the same interpretation across possible worlds — and thus provide support for the standard rigid quantification in modal logic — and flexible symbols, whose interpretation may vary;
(c) third, we use modal operators over dynamic-logic actions, which are defined as regular expressions over binary nominal relations.
In this context, we propose a general notion of hybrid-dynamic Horn clause and develop a proof calculus for the Horn-clause fragment of hybrid-dynamic first-order logic. We investigate soundness and compactness properties for the syntactic entailment system that corresponds to this proof calculus, and prove a Birkhoff-completeness result for hybrid-dynamic first-order logic.

14:30 – 15:00 Walter Guttmann(JSPS International Research Fellow /
University of Canterbury, New Zealand)
演題: Algebras for Minimum Spanning Tree Problems
概要: Relation-algebraic methods have been used to develop algorithms for unweighted graphs. This works well because unweighted graphs can be directly represented as relations. We study a generalization of relation algebras in which the underlying Boolean algebra structure is replaced with a Stone algebra. The generalized algebras model weighted graphs, which do not have direct representations as binary relations. Using the new algebras we prove the correctness of Prim’s and Kruskal’s minimum spanning tree algorithms. We show that these algorithms solve various optimization problems with different aggregation functions, not just the original problem they were designed for.The proofs are formally verified in Isabelle/HOL, including the overall Hoare-logic argument, algebraic theories, calculations and models.

15:20 – 15:50 古澤 仁(鹿児島大学)
演題: On Continuity of Relations
概要: This talk provides 4 equivalent conditions with
the continuity of relations adopted by Brattka and Hertling
to investigate computability of relations. As the case of
continuous functions, each condition characterizes continuous
relations by respectively using open sets, neighborhoods,
closures, and closed sets. A notion of sequential continuity
is also studied. We show a relevance between continuous relations
and sequentially continuous relations which is, again,
analogous to the case of functions.

16:10 – 16:40 河原康雄(九州大学名誉教授)
演題: 関係計算の歴史をふりかえる
概要: 関係計算の約170年の歴史を独断と偏見を交え振り返り、これからの研究の糧としたい。

17:00 –  18:00 自由討論

問合せ先: 溝口佳寛 (九州大学マス・フォア・インダストリ研究所)
ym @ imi.kyushu-u.ac.jp

科学研究費補助金 基盤研究C 課題番号:17K05346 研究代表者:溝口佳寛,


次の通り,第17回 論理と計算セミナーを計画しています.

日時: 2018年 9月 2日 (月) 16:00〜18:00(予定)
場所: 福岡工業大学 FITセミナーハウス(大分県由布市湯布院町)
参加費:基本無料ですが, 宿泊される場合は,第2回論理と計算サマースクールの参加費が必要.

  • 16:00–16:30
  • 16:30–17:00
  • 17:00–17:30

第16回 論理と計算セミナー

次の通り、第16回 論理と計算セミナーを計画しています。

日時: 2018年 9月 3日 (月) 16:30〜18:00
場所: 福岡工業大学 FITセミナーハウス(大分県由布市湯布院町)

  1. Brett McLean (University College London, 学振特別研究員(サマープログラム)):Algebraic reasoning for functions
  2. 溝口佳寛(九大IMI・数理・データサイエンス教育センター):九州大学数理・データサイエンス教育研究センターと AIMaP 事業について
  3. 井口修一 (福岡工業大学 情報工学部):1次元CAで実現する奇偶ソートについて




井口修一( inokuchi (at) fit.ac.jp )

第15回 論理と計算セミナー

日時: 2017年 2月 17日 (金) 14:00〜
場所: 鹿児島大学理学部2号館5階502
 ( https://www.kagoshima-u.ac.jp/about/campusmap.html )


  • 14:00 — 14:30  森 雅生(東京工業大学):関手データモデルに関する実務的見解
  • 14:30 — 15:00  中村誠希(東京工業大学):KleeneのAntimirov偏微分について
  • 15:00 — 15:15  [休憩]
  • 15:15 — 15:45 西澤弘毅(神奈川大学):Multi-valued multirelations
  • 15:45 — 16:15 河原康雄(九州大学):関係の連続性と陰関数の定理
  • 16:15 — 16:30  [休憩]
  • 16:30 — 17:00 田中義人(九州産業大学):Semilattices with operatorsのquasi-identities
  • 17:00 — 18:00  自由討論(当日飛び入り講演OKです!)
  • 18:30 — 懇親会


The 14th Logic and Computation Seminar

Date: 2015-11-12 13:00-16:50
Place: Momochi Office, Institute of Mathematics for Industry, Kyushu University
3F, Industry-University-Government Collaboration Innovation Plaza,
3-8-34 Momochihama Sawara-ku, Fukuoka, JAPAN)
( http://imaq.kyushu-u.ac.jp/ja/imaq/access.php )


  • 13:00-13:10 (Opening)

  • 13:10-13:50
    Verification of Relational Programs and Approximation Algorithms
    Peter Höfner (NICTA, Australia)

  • 14:00-14:40
    Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm
    Walter Guttmann (Univ. Canterbury, New Zealand)

  • 14:50-15:30
    Axiom of choice and Zorn’s lemma in Dedekind 
    Yasuo Kawahara (Kyushu Univ., Japan)

  • 15:40-16:10
    A Certified Wang Tiling Program with the Coq Proof Assistant
    Toshiaki Matsushima (Kyushu Univ., Japan)

  • 16:20-16:50
    Origami System using CGA
    Mitsuhiro Kondo, Takuya Matsuo (Kyushu Univ., Japan)
  • 16:50 (Closing)

If you have any inquiry, please let me (ym @ imi.kyushu-u.ac.jp) know.

第13回 論理と計算セミナー

日時: 2015年 7月 4日 (土) 14:00〜 
場所: 福岡工業大学 情報工学部 システムマネジメント学科 演習室3 B棟8階
( http://www.fit.ac.jp/daigaku/gaiyo/koutsu )


  1. 14:00-15:00 河原康雄(九州大学名誉教授)
    モノイド上の CA に対する GOE 定理
  2. 15:10-15:40 森雅生(東京工業大学)
    Logic, Data Science and Institutional Research
  3. 15:40-16:10 正代隆義(九州国際大学)
  4.  16:20-16:50 松嶋聡昭(九州大学数理学研究院)
    Coq 関係計算ライブラリの開発
  5.  16:50-17:20 津曲紀宏(崇城大学)
    Algebras of Convex relations
  6. 17:20-17:50 田中義人(九州産業大学)
    Degree 1の論理式で定まるELのあるクラスの代数モデル

18:30- 懇親会 (竹乃屋千早駅前店)



第12回 論理と計算セミナー

日時: 2014年 9月 1日 (金) 午後
場所: 福岡工業大学 情報工学部 システムマネジメント学科 演習室3 B棟8階
( http://www.fit.ac.jp/daigaku/gaiyo/koutsu )

丸山 勲(福岡工業大学情報工学部情報システム工学科)
石田 俊一(九州産業大学基礎教育センター)
田中 義人(九州産業大学経済学部)
田中 久治(佐賀大学)


  1. 13:00-13:50 丸山 勲(福岡工業大学情報工学部情報システム工学科)
    – 密度行列繰り込み群,ベーテ仮説,Z2トポロジカル不変量 –
  2. 14:00-14:50 石田 俊一(九州産業大学基礎教育センター)
    Cellular Automata Defined by Formulae on Monoids
  3. 15:10-16:00 田中 義人(九州産業大学経済学部)
  4. 16:10-17:00 MOHAMMAD DENI AKBAR(九州大学数理学府)
    Fuzzy Relational Database Model Using Fuzzy Relational Calculus
  5. 17:10-17:40 田中久治(佐賀大学)
    初等幾何学のCoqによる証明(Area Method on Coq)