Verification Series

Local Reductions for Modal Logic

26th May 2023, 11:00 add to calender
Ullrich Husdadt

Abstract

The modal logic K is commonly used to represent and reason about
necessity and possibility and its extensions with combinations of
additional axioms are used to represent knowledge, belief, desires and
intentions. I will present local reductions of all propositional modal
logics in the so-called modal cube, that is, extensions of K with
arbitrary combinations of the axioms B, D, T, 4 and 5 to a normal form
comprising a formula and the set of modal levels it occurs at. We can
then further transform formulae in this normal form back to K, thereby
allowing arbitrary decision procedures for K to be used for reasoning in
all the logics of the modal cube.
add to calender (including abstract)