Solving quantified modal logic problems by translation to classical logics

DOI10.1093/LOGCOM/EXAF006MaRDI QIDQ6909867zbMATH OpenFDO

Authors Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller

Publication date 29 October 2025

Published in Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/LOGCOM/EXAF006

zbMATH Keywords

automated theorem provingfirst-order logichigher-order logicnon-classical logicsquantified modal logics

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX) Computer science (68-XX)

Cites work

• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• A combinator-based superposition calculus for higher-order logic
• A formulation of the simple theory of types.
• A Functional calculus of first order based on strict implication
• An empirical assessment of progress in automated theorem proving
• Completeness in the theory of types
• Computer supported mathematics with MEGA
• Efficient local reductions to basic modal logic
• Faster, higher, stronger: E 2.3
• First-order modal logic
• Folding domain-specific languages: deep and shallow embeddings (functional pearl)
• General models and extensionality
• Grundgesetze der Arithmetik. Begriffsschriftlich abgeleitet. I. Band.
• Handbook of epistemic logic
• Higher-order semantics and extensionality
• HOL Based First-Order Modal Logic Provers
• scientific article; zbMATH DE number 1612541 (Why is no real title available?)
• scientific article; zbMATH DE number 5850137 (Why is no real title available?)
• scientific article; zbMATH DE number 1950267 (Why is no real title available?)
• scientific article; zbMATH DE number 1765691 (Why is no real title available?)
• scientific article; zbMATH DE number 7015113 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• scientific article; zbMATH DE number 3325547 (Why is no real title available?)
• Implementing and evaluating provers for first-order modal logics
• Isabelle/HOL. A proof assistant for higher-order logic
• Making higher-order superposition work
• MleanCoP: a connection prover for first-order modal logic
• Modal logic
• Modality and quantification in S5
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Quantified multimodal logics in simple type theory
• Semantics-Based Translation Methods for Modal Logics
• Solving modal logic problems by translation to higher-order logic
• The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
• The higher-order prover Leo-III
• The logic languages of the TPTP world
• The QMLTP problem library for first-order modal logics
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Theorem provers for every normal modal logic
• TPTP, TSTP, CASC, etc.

Cited in

(3)

• On structures of sign-boundary and diagonal vacancy-type standard contradictions
• Faithful logic embeddings in HOL -- deep and shallow
• Dependently typed higher-order logic

This page was built for publication: Solving quantified modal logic problems by translation to classical logics

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