Verification Series
Local Reductions for Modal Logic
26th May 2023, 11:00
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.
Ashton Street, Liverpool, L69 3BX
United Kingdom
Call the department
+44 (0)151 795 4275