@ARTICLE{SchmidtHustadt07a,
AUTHOR = {Schmidt, R. A. and Hustadt, U.},
YEAR = {2007},
TITLE = {The Axiomatic Translation Principle for Modal Logic},
JOURNAL = {ACM Transactions on Computational Logic},
VOLUME = {8},
NUMBER = {4},
PAGES = {1--55},
URL = {url{http://www.cs.man.ac.uk/~schmidt/publications/SchmidtHustadt07a.html}},
DOI = {http://doi.acm.org/10.1145/1276920.1276921},
ABSTRACT = {In this paper we present a translation principle, called the
\emph{axiomatic translation}, for reducing propositional modal logics
with background theories, including
triangular properties such as transitivity, Euclideanness and
functionality, to decidable fragments of first-order logic.
The goal of the axiomatic translation principle is to
find simplified theories, which
capture the inference problems in the original theory, but in a way
that can be readily automated and is easier to deal with by existing
(first-order) theorem provers than the standard translation.
The principle of the axiomatic translation is conceptually very simple
and can be almost completely automated.
Soundness is automatic under reasonable assumptions, general
decidability results can be stated and termination of ordered
resolution is easily achieved.
The non-trivial part of the approach is proving completeness.
We prove results of completeness, decidability, model generation, 
the small model property and the interpolation property for a number 
of common and less common modal logics.
We also present results of experiments with a number of first-order
logic theorem provers which are very encouraging.
},
}