MiG

Quantified Multimodal Logics in Simple Type Theory

Christoph Benzmüller, L.C. Paulson— 2012

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.

TitelQuantified Multimodal Logics in Simple Type Theory
VerfasserChristoph Benzmüller, L.C. Paulson
VerlagLogica Universalis (Special Issue on Multimodal Logics), Springer-Verlag
Datum2012
KennungISSN: 1661-8297; doi: 10.1007/s1787-012-0052-y
Quelle/n
Spracheeng
ArtText