Quantified multimodal logics in simple type theory
From MaRDI portal
Publication:1945702
DOI10.1007/s11787-012-0052-yzbMath1334.03014OpenAlexW1807678626WikidataQ57382584 ScholiaQ57382584MaRDI QIDQ1945702
Christoph Benzmüller, Lawrence Charles Paulson
Publication date: 8 April 2013
Published in: Logica Universalis (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s11787-012-0052-y
Related Items
Cut-elimination for quantified conditional logic, The higher-order prover \textsc{Leo}-II, Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics, Interacting with Modal Logics in the Coq Proof Assistant, Extensional higher-order paramodulation in Leo-III, Computer-Supported Analysis of Arguments in Climate Engineering, The MET: The Art of Flexible Reasoning with Modalities, The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Solving modal logic problems by translation to higher-order logic, Formalising basic topology for computational logic in simple type theory, Higher-Order Modal Logics: Automation and Applications, Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument, Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support, Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments, Computer-assisted analysis of the Anderson-Hájek ontological controversy, Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- TPS: A hybrid automatic-interactive system for developing proofs
- Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings
- Terminating tableau systems for hybrid logic with difference and converse
- Types, tableaus, and Gödel's God
- Isabelle/HOL. A proof assistant for higher-order logic
- An introduction to mathematical logic and type theory: To truth through proof.
- First-order modal logic
- Failures of the interpolation lemma in quantified modal logic
- Multimodal and intuitionistic logics in simple type theory
- Interpolation for first order S5
- A completeness theorem in modal logic
- Intensional models for the theory of types
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A Brief Overview of HOL4
- Propositional quantifiers in modal logic1
- On the complexity of propositional quantification in intuitionistic logic
- Higher-order semantics and extensionality
- On modal logic with propositional quantifiers
- General models, descriptions, and choice in type theory
- General models and extensionality
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- A formulation of the simple theory of types
- Completeness in the theory of types
