Quantified multimodal logics in simple type theory
From MaRDI portal
Publication:1945702
Recommendations
- Multimodal and intuitionistic logics in simple type theory
- Combining and automating classical and non-classical logics in classical higher-order logics
- Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
- Combining logics in simple type theory
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
Cites work
- A Brief Overview of HOL4
- A completeness theorem in modal logic
- A formulation of the simple theory of types
- An introduction to mathematical logic and type theory: To truth through proof.
- Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings
- Completeness in the theory of types
- Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
- Failures of the interpolation lemma in quantified modal logic
- First-order modal logic
- General models and extensionality
- General models, descriptions, and choice in type theory
- Higher-order semantics and extensionality
- scientific article; zbMATH DE number 755666 (Why is no real title available?)
- Intensional models for the theory of types
- Interpolation for first order S5
- Isabelle/HOL. A proof assistant for higher-order logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Multimodal and intuitionistic logics in simple type theory
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- On modal logic with propositional quantifiers
- On the complexity of propositional quantification in intuitionistic logic
- Propositional quantifiers in modal logic1
- Terminating tableau systems for hybrid logic with difference and converse
- TPS: A hybrid automatic-interactive system for developing proofs
- Types, tableaus, and Gödel's God
Cited in
(35)- The \(HOL\) logic extended with quantification over type variables
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Cut-elimination for quantified conditional logic
- Extensional higher-order paramodulation in Leo-III
- A Multi-type Calculus for Inquisitive Logic
- The higher-order prover \textsc{Leo}-II
- Higher-order modal logics: automation and applications
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Multimodal and intuitionistic logics in simple type theory
- Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
- Interacting with Modal Logics in the Coq Proof Assistant
- Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- Combining logics in simple type theory
- GoedelGod
- scientific article; zbMATH DE number 7561490 (Why is no real title available?)
- Computer-supported analysis of arguments in climate engineering
- Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel's ontological argument
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Lowe_Ontological_Argument
- PLM
- scientific article; zbMATH DE number 3273876 (Why is no real title available?)
- The MET: The Art of Flexible Reasoning with Modalities
- Solving modal logic problems by translation to higher-order logic
- Formalising basic topology for computational logic in simple type theory
- Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments
- Faithful logic embeddings in HOL -- deep and shallow
- Notes on Gödel's and Scott's variants of the ontological argument
- Semantical investigations on non-classical logics with recovery operators: negation
- Solving quantified modal logic problems by translation to classical logics
- Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
- Types, Tableaus and Gödel’s God in Isabelle/HOL
- Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL
- Anselm's God in Isabelle/HOL
This page was built for publication: Quantified multimodal logics in simple type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1945702)
