HOL Based First-Order Modal Logic Provers

DOI10.1007/978-3-642-45221-5_9MaRDI QIDQ2870120zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Implementing and evaluating provers for first-order modal logics
• A proof theoretic tool for first-order modal logic
• The first-order hypothetical logic of proofs
• scientific article; zbMATH DE number 1301858
• A sequent calculus for first-order logic formalized in Isabelle/HOL
• On the proof-theory of two formalisations of modal first-order logic
• First-order modal logic
• First-order modal logic
• First-order resolution methods for modal logics

Cited in

(9)

• Solving modal logic problems by translation to higher-order logic
• scientific article; zbMATH DE number 1341605 (Why is no real title available?)
• Extensional higher-order paramodulation in Leo-III
• Implementing and evaluating provers for first-order modal logics
• FMLtoHOL
• Higher-order modal logics: automation and applications
• Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
• Solving quantified modal logic problems by translation to classical logics
• Preface: Special issue on logic and argumentation

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2870120)