@PHDTHESIS{Schmidt97d,
AUTHOR = {Schmidt, R. A.},
YEAR = {1997},
TITLE = {Optimised Modal Translation and Resolution},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken, Germany},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/Schmidt97d.html},
ABSTRACT = {This thesis studies the optimised functional translation of
propositional modal logics to first-order logic, and first-order
resolution as a means for realising modal reasoning.
The optimised functional translation maps modal logics to a lattice of
clausal logics, called path logics.
The general apparatus of inference for path logics is theory resolution.
We show that satisfiability in basic path logic and certain extensions can
be decided by resolution and condensing without requiring additional
refinement strategies.
We propose an improved theory unification algorithm for \textit{S4}, and we
present a calculus of ordered $E$-resolution with normalisation.
We show also that some essentially second-order modal logics convert to
path logics, which can be exploited for accomodating inference for
modal logics with numerical quantifiers in a calculus of resolution and
simple arithmetic.
}
}