Two of our departmental visitors will give short seminar talks next Wednesday:
|Who: || Claudia Nalon and Clemens Kupke
Where: || RSISE Seminar Room, Ground Floor, RSISE Building 115
|When: || Wednesday Feb 3, 14:30
|What:|| CN: Modal-Layered Resolution for Multimodal K
| CK: Coalgebraic Dynamic Logics
All welcome -- abstracts below.
Modal-Layered Resolution for Multimodal K
We present a modal-layered, clausal hyper-resolution calculus for the basic multimodal logic K, which divides the clause set according to the modal layer at which clauses occur. Some refinements, as negative and ordered resolution, can also be used to further restrict the search for a proof. We will also briefly describe an implementation
on of the calculus and present experimental results.
Coalgebraic Dynamic Logics
I will present a (co)algebraic framework that allows to study dynamic
modal logics such as Propositional Dynamic Logic (PDL) and Game Logic
(GL) in a uniform way. The main observation is that the program/game
constructs of PDL/GL arise from monad structure, and the axioms of these
logics correspond to certain compatibility requirements between the
modalities and this monad structure. This leads to a general soundness
and completeness result for PDL-like logics for T-coalgebras where T is
a monad and the program constructs are given by sequential composition,
test, and pointwise extensions of operations of T.
(Joint work with Helle Hvid Hansen.)