The lecture will start with a brief introduction to basic modal logic. Then
we move
on to a review of my hovedfag thesis.

We look at how proof trees for propositional modal formulae can be built
using falsification rules.
The rules obviously depend on what kind of modal system we work with (K, K4,
KT etc.). A many-sorted language for formulating such rules is defined. This
language serves two purposes:

1. It allows the user to formulate the rules for an automatic theorem
prover.
2. It gives rise to a meta-logic that allows us to reason about such things
as equivalency between rules and inclusion of a schema in a given logic.
Admittedly, this meta-logic is probably very weak.

In addition several questions can be asked in light of the rule
formulations -
key words are for example: ways to categorize modal logics, terminating
proofs, definability.