Quantified Multimodal Logics in Simple Type Theory
Artificial Intelligence
2009-05-18 v1 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.0905.2435,
title = {Quantified Multimodal Logics in Simple Type Theory},
author = {Christoph Benzmueller and Lawrence C. Paulson},
journal= {arXiv preprint arXiv:0905.2435},
year = {2009}
}
Comments
ii + 22 pages