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

Authors
Christoph Benzmueller
Freie Universität Berlin
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
Keywords Quantified multimodal logics  simple type theory  semantic embedding  proof automation
Categories (categorize this paper)
DOI 10.1007/s11787-012-0052-y
Options
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: 65,740
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.
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 (2):56-68.

View all 29 references / Add more references

Citations of this work BETA

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.
Cut-Elimination for Quantified Conditional Logic.Christoph Benzmüller - 2017 - Journal of Philosophical Logic 46 (3):333-353.

View all 6 citations / Add more citations

Similar books and articles

Analytics

Added to PP index
2013-03-10

Total views
122 ( #90,714 of 2,462,951 )

Recent downloads (6 months)
1 ( #449,363 of 2,462,951 )

How can I increase my downloads?

Downloads

My notes