Higher-Order Modal Logics: Automation and Applications
From MaRDI portal
Publication:2970308
DOI10.1007/978-3-319-21768-0_2zbMath1358.68273OpenAlexW1448681095MaRDI QIDQ2970308
Christoph Benzmüller, Bruno Woltzenlogel Paleo
Publication date: 30 March 2017
Published in: Reasoning Web. Web Logic Rules (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-21768-0_2
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
Variants of Gödel's ontological proof in a natural deduction calculus ⋮ The higher-order prover \textsc{Leo}-II ⋮ Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics ⋮ Formalizing the unexpected hanging paradox: a classical surprise ⋮ Para-Disagreement Logics and Their Implementation Through Embedding in Coq and SMT ⋮ Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Learning-assisted theorem proving with millions of lemmas
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Comparing formal theories of context in AI
- A curious inference
- Simplified semantics for basic relevant logics
- A semantical analysis of the calculi \(C_n\)
- Multilanguage hierarchical logics, or: How we can do without modal logics
- Types, tableaus, and Gödel's God
- Isabelle/HOL. A proof assistant for higher-order logic
- Handbook of philosophical logic. Vol. 6
- First-order modal logic
- Quantified multimodal logics in simple type theory
- The locally nameless representation
- HOL(y)Hammer: online ATP service for HOL Light
- Extending Sledgehammer with SMT solvers
- Premise selection for mathematics by corpus analysis and kernel methods
- Propositional calculus for contradictory deductive systems
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- HOL Based First-Order Modal Logic Provers
- Satallax: An Automatic Higher-Order Prover
- The QMLTP Problem Library for First-Order Modal Logics
- Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners)
- MleanCoP: A Connection Prover for First-Order Modal Logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Generality in artificial intelligence
- On sets, types, fixed points, and checkerboards
- Higher-order semantics and extensionality
- Logic-Free Reasoning in Isabelle/Isar
- General models and extensionality
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- Completeness in the theory of types
This page was built for publication: Higher-Order Modal Logics: Automation and Applications
