Resolution for some first-order modal systems (Q1178699)

In the wake of growing interest among computer scientists in intensional logics one of the problem fields is to make such logics accessible for automated deduction methods. Building on earlier approaches toward the propositional case the author develops the resolution method for the first-order modal logics \(D\) (the ``denotic \(T\)''), \(T\), and \(S4\) up to an outline of the completeness and soundness proof of that method.