Quantified Multimodal Logics in Simple Type Theory

Simple item page
dc.creatorBenzmueller, Christoph
dc.creatorPaulson, Lawrence C.
dc.date2009-05-14
dc.date.accessioned2026-07-07T13:15:33Z
dc.date.available2026-07-07T13:15:33Z
dc.descriptionWe 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.
dc.descriptionii + 22 pages
dc.identifierhttps://arxiv.org/abs/0905.2435
dc.identifierhttp://arxiv.org/abs/0905.2435
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/230501
dc.subjectArtificial Intelligence
dc.subjectLogic in Computer Science
dc.subjectI.2.4; I.2.3; F.4.1
dc.titleQuantified Multimodal Logics in Simple Type Theory
dc.typetext

Files

Collections

arXiv