Model construction for modal clauses

DOI10.1007/978-3-031-63501-4_1MaRDI QIDQ7034600zbMATH OpenFDO

Authors Ullrich Hustadt, Fabio Papacchini, Cláudia Nalon, Clare Dixon

Publication date 31 January 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-63501-4_1

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• A guide to completeness and complexity for modal logics of knowledge and belief
• A Machine-Oriented Logic Based on the Resolution Principle
• A Modal-Layered Resolution Calculus for K
• Application of modal logic to programming
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Blocking and other enhancements for bottom-up model generation methods
• Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
• Cardinality restrictions on concepts
• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• Clausal resolution for normal modal logics
• Constructing Bachmair-Ganzinger models
• First-order resolution methods for modal logics
• scientific article; zbMATH DE number 3848604 (Why is no real title available?)
• scientific article; zbMATH DE number 67503 (Why is no real title available?)
• scientific article; zbMATH DE number 140411 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• InKreSAT: modal reasoning via incremental reduction to SAT
• Modal Resolution
• Never trust your solver: certification for SAT and QBF
• Optimized description logic reasoning via core blocking
• Resolution theorem proving
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
• Terminating minimal model generation procedures for propositional modal logics
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• Using tableau to decide description logics with full role negation and identity
• Verified Decision Procedures for Modal Logics.
• Verifying concurrent processes using temporal logic

This page was built for publication: Model construction for modal clauses

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