Datensatz

Zusammenfassung

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.