@book{SR--2009--02,
year={2009},
author={Benzm{\"u}ller, Christoph
    and Paulson, Lawrence C.},
title={Quantified Multimodal Logics in Simple Type Theory},
series={{SEKI Report SR--2009--02 (ISSN 1437--4447)}},
note={{\url{http://arxiv.org/abs/0905.2435}}},
abstract={We present a straightforward embedding of quantified multimodal logic in simple type theory and prove its soundness and completeness. Modal operators are replaced by quantification over a type of possible worlds. We present simple experiments, using existing higher-order theorem provers, to demonstrate that the embedding allows automated proofs of statements in these logics, as well as meta properties of them.},
publisher={{SEKI Publications}},
address={{DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str.\,5, D--28359 Bremen, Germany}},
}