The Splitting Theorem for finitely generated Propositional Dynamic Logic

Adam Mata

supervisor: Anna Zamojska-Dzienio



Modal logic as a branch of mathematics has been widely developed during the end of the previous century. It provides multiple tools for different branches of computer science: modelling the progation of knowledge in agent systems, building atomated-proovers, and validating correctness of computer programs. The latter problem has given birth to the extension of Modal Logic – namely Dynamic Logic, which provides machinery for reasoning about logical structures where validity of formula may change dynamically.

Around 1980 the collection of extensions of Modal Logic was examined to find properties which are similar among them. Algebraical methods applied to this issue allowed to, firstly, create a mathematical structure of these extensions – the lattice. Secondly, The Splitting Theorem ocurred, which treats about pairs of extensions which somehow „split” the lattice into two mutually complementing parts.

The recent research concerning the extensions of Dynamic Logic itself has shown that Kleene’s Algebras, which are semantical structures for Dynamic Logic, also form the lattice. Nevertheless, there are no results stating about splitting this lattice. The goal of the research is to characterize complementing pairs of finite extensions of Propositional Dynamic Logics, which split the mentioned lattice by algebraical and domain-theory methods.