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

Christoph Benzmueller
Freie Universität Berlin
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
Keywords Quantified multimodal logics  simple type theory  semantic embedding  proof automation
Categories (categorize this paper)
DOI 10.1007/s11787-012-0052-y
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 53,682
Through your library

References found in this work BETA

A Completeness Theorem in Modal Logic.Saul A. Kripke - 1959 - Journal of Symbolic Logic 24 (1):1-14.
First-Order Modal Logic.Roderic A. Girle, Melvin Fitting & Richard L. Mendelsohn - 2002 - Bulletin of Symbolic Logic 8 (3):429.
First Order Modal Logic.Melvin Fitting & Richard Mendelsohn - 2001 - Studia Logica 68 (2):287-289.

View all 29 references / Add more references

Citations of this work BETA

Cut-Elimination for Quantified Conditional Logic.Christoph Benzmüller - 2017 - Journal of Philosophical Logic 46 (3):333-353.
The Totality of Predicates and the Possibility of the Most Real Being.Srećko Kovač - 2018 - Journal of Applied Logics - The IfCoLog Journal of Logics and Their Applications 5 (7):1523-1552.

View all 6 citations / Add more citations

Similar books and articles


Added to PP index

Total views
118 ( #78,899 of 2,349,382 )

Recent downloads (6 months)
9 ( #72,212 of 2,349,382 )

How can I increase my downloads?


My notes