ymizoguchi のすべての投稿

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 研究代表者:溝口佳寛,

第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 )

第1回 論理と計算サマースクール


場所:福岡工業大学 FITセミナーハウス(大分県由布市湯布院町)

13:00 — 14:15 LCSS 1
14:30 — 16:00 LCSS 2
16:30 — 18:00 第16回 論理と計算セミナー
20:00 — 22:00 自由討論
9:00 — 11:00 LCSS 3

LCSS 1 : (座長:九産大)

  1. 杉本実奈美(福工大シスマネ):地震シミュレーションへ向けた砂山モデルの改良
  2. 井町 信ノ輔(九産大情報科学):性格特性を考慮したグループワークへのICT活用と効果の関係性について
  3. 竹繁花音(大分大教育福祉科学部):貯金支援アプリ 貯金でつくるアクアリウム
  4. 山崎 大源(九産大情報科学):睡眠とスマートフォンの利用状況における関係性の解析と可視化について
  5. 浅野佑弥(九大数理):Laplacian Eigenfunctionsを用いた流体シミュレーションの実装

LCSS 2 : (座長:大分大)

  1. 首藤真也(大分大教育福祉科学部):野球スコア集計Webサイトの開発
  2. 森下茄穂(福工大シスマネ):雪の結晶CAにおけるルールが与える影響について
  3. 坂口 涼平(九産大情報科学):理系学生の授業外学習のICTを使った支援システム及び利用法に関する考察
  4. 松藤ちひろ(九大数理):3次元モデルの変形補間について
  5. 綾部百合子(福工大シスマネ):2x2x2ルービックキューブの解析について
  6. 佐々野 俊太郎(九産大情報科学):コミュニケーション向上に向けた取り組みへのICT活用支援と効果の可視化について

LCSS 3 : (座長:福工大)

  1. 月原大貴&山田凌(福工大シスマネ):一斉射撃問題の量子化に向けて
  2. 後藤大輝(大分大教育福祉科学部):高齢者の低栄養改善アプリの開発
  3. 中島康晴(福工大シスマネ):コンビニエンスストアにおけるPOP広告の有効性
  4. 井上 拓哉(九産大情報科学):CAを用いた暗号化システムの構築に関する研究
  5. 平野仁蒔穂(大分大教育福祉科学部):声で予定を知らせる録音機能付きアラームアプリの開発
  6. 衛藤優汰(福工大シスマネ):3次元迷路の作成について







井口修一(福工大.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- 懇親会 (竹乃屋千早駅前店)