Date: Friday, 15 November 2019, 13:30-18:00
Place: Nishijin Plaza, Multi-purpse Room(2-16-23 Nishijin, Sawara-ku, Fukuoka-shi)
http://nishijinplaza.kyushu-u.ac.jp/english/index.php
Program:
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
第18回論理と計算セミナー
日時: 2019年11月15日(金) 13:30-18:00
場所: 九州大学西新プラザ多目的室 (福岡市早良区西新2-16-23)
http://nishijinplaza.kyushu-u.ac.jp/index.php
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 河原康雄（九州大学名誉教授）
演題: 関係計算の歴史をふりかえる
概要: 関係計算の約１７０年の歴史を独断と偏見を交え振り返り、これからの研究の糧としたい。
17:00 – 18:00 自由討論
問合せ先: 溝口佳寛 (九州大学マス・フォア・インダストリ研究所)
ym @ imi.kyushu-u.ac.jp
※この研究集会の一部は
科学研究費補助金 基盤研究C 課題番号:17K05346 研究代表者:溝口佳寛,
の支援のもと開催されます。
論理と計算 