Quantified Multimodal Logics in Simple Type Theory

Logica Universalis 7 (1):7-20 (2013)
  Copy   BIBTEX

Abstract

We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,088

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2013-03-10

Downloads
141 (#124,650)

6 months
5 (#311,051)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Christoph Benzmueller
Freie Universität Berlin

References found in this work

A New Introduction to Modal Logic.M. J. Cresswell & G. E. Hughes - 1996 - New York: Routledge. Edited by M. J. Cresswell.
A completeness theorem in modal logic.Saul Kripke - 1959 - Journal of Symbolic Logic 24 (1):1-14.
A formulation of the simple theory of types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
Completeness in the theory of types.Leon Henkin - 1950 - Journal of Symbolic Logic 15 (2):81-91.
A Formulation of the Simple Theory of Types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (3):114-115.

View all 29 references / Add more references