Higher-Order Modal Logics: Automation and Applications

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

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35)

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

• Unnamed Item
• Unnamed Item
• Unnamed Item
• TPTP
• Sledgehammer
• QMLTP
• HOLyHammer
• AgsyHOL
• MleanCoP
• FMLtoHOL
• GitHub

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