Springe direkt zu Inhalt

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.

Titel
Quantified Multimodal Logics in Simple Type Theory
Verfasser
Christoph Benzmüller, L.C. Paulson
Verlag
Logica Universalis (Special Issue on Multimodal Logics), Springer-Verlag
Datum
2012
Kennung
ISSN: 1661-8297; doi: 10.1007/s1787-012-0052-y
Quelle/n
Sprache
eng
Art
Text