Mohr, Erik

Resolution-Based Calculi for Modal Logics

Based on different translation approaches from first-order modal logic into
first-order predicate logic we develop several kinds of resolution-based calculi
with additional theory clauses, inference rules or special unification algorithms.
Especially the methods presented for the semi-functional and functional approaches
lead to limited branching in the proof search tree and therefore to smaller sets
of generated clauses. In all cases soundness and (refutation) completeness proofs
for these calculi are provided. The methods have been applied to serial modal
logics (i.e. modal logics containing the so-called axiom D) with constant, (and
partially) varying, increasing and decreasing domain structures and any
combination of the following modal logic axioms: T, B, 4 and 5.