HOL Based First-Order Modal Logic Provers

DOI10.1007/978-3-642-45221-5_9zbMath1406.68103OpenAlexW2268873381MaRDI QIDQ2870120

Christoph Benzmüller, Thomas Raths

Publication date: 17 January 2014

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-45221-5_9

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Related Items (5)

Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Solving modal logic problems by translation to higher-order logic ⋮ Higher-Order Modal Logics: Automation and Applications ⋮ FMLtoHOL

Uses Software

• LEO-II
• Nitpick
• Isabelle/HOL
• TPTP
• Satallax
• leanCoP
• ileanCoP
• QMLTP
• AgsyHOL
• MSPASS

This page was built for publication: HOL Based First-Order Modal Logic Provers