Advocates logical pluralism at the object level inside a unifying HOL meta-framework to enable interdisciplinary reuse and warns against single-logic imperialism.
Quantified Multimodal Logics in Simple Type Theory
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
abstract
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.
fields
cs.LO 1years
2026 1verdicts
UNVERDICTED 1representative citing papers
citing papers explorer
-
Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)
Advocates logical pluralism at the object level inside a unifying HOL meta-framework to enable interdisciplinary reuse and warns against single-logic imperialism.