@TECHREPORT{SchmidtHustadt04a,
AUTHOR = {Schmidt, R. A. and Hustadt, U.},
YEAR = {2004},
TITLE = {A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae},
TYPE = {Preprint Series},
NUMBER = {CSPP-22},
INSTITUTION = {University of Manchester},
ADDRESS = {UK},
NOTE = {Long version of \cite{SchmidtHustadt03b}},
URL = {\url{http://www.cs.man.ac.uk/~schmidt/publications/SchmidtHustadt04a.html}},
ABSTRACT = {In this paper we present a translation principle, called the
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 is more amenable to automation and easier to deal
with by existing (first-order) theorem provers.  The principle
of the axiomatic translation is conceptually very simple and
can be largely automated.  Soundness is automatic under
reasonable assumptions, and termination of ordered resolution
is easily achieved; the non-trivial part of the approach is
proving completeness.},
}