非表示:
キーワード:
-
要旨:
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.
