Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners)
From MaRDI portal
Publication:3058454
DOI10.1007/978-3-642-17172-7_7zbMath1309.68166OpenAlexW1499361683MaRDI QIDQ3058454
Publication date: 22 November 2010
Published in: Verification, Induction, Termination Analysis (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-17172-7_7
Related Items
Embedding and automating conditional logics in classical higher-order logic, Higher-Order Modal Logics: Automation and Applications, Combining and automating classical and non-classical logics in classical higher-order logics
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- TPS: A hybrid automatic-interactive system for developing proofs
- Solving the \$100 modal logic challenge
- Terminating tableau systems for hybrid logic with difference and converse
- Isabelle/HOL. A proof assistant for higher-order logic
- Natural deduction for first-order hybrid logic
- An introduction to mathematical logic and type theory: To truth through proof.
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Multimodal and intuitionistic logics in simple type theory
- Interpolation for first order S5
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- Combining Logics in Simple Type Theory
- Higher-order semantics and extensionality
- 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
- Analytic Tableaux for Higher-Order Logic with Choice
- A formulation of the simple theory of types
- Completeness in the theory of types
