Quantified Multimodal Logics in Simple Type Theory

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

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.
ii + 22 pages

Keywords

Artificial Intelligence, Logic in Computer Science, I.2.4; I.2.3; F.4.1

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/230501

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/0905.2435
 http://arxiv.org/abs/0905.2435

Collections

arXiv