Deciding Extended Modal Logics by Combining State Space Generation and SAT Solving

DOI10.1007/978-3-319-99957-9_8MaRDI QIDQ6108819zbMATH OpenFDO

Authors Martin Strecker

Publication date 30 June 2023

Published in Artificial Intelligence and Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-99957-9_8

zbMATH Keywords

automated theorem provinggraph transformationsmodal logicprogram verification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Modal Satisfiability via SMT Solving
• Theory and Applications of Relational Structures as Knowledge Instruments
• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• Resolution-based methods for modal logics
• Decidability by resolution for propositional modal logics

Cites work

• A Hoare-like calculus using the \(\mathrm{SROIQ}^{\sigma }\) logic on transformations of graphs
• Automated reasoning in \(\mathcal{ALCQ}\) via SMT
• Automated reasoning in modal and description logics via SAT encoding: the case study of \(K_m/\mathcal{ALC}\)-satisfiability
• Modal Satisfiability via SMT Solving
• Revisiting enumerative instantiation
• SAT-based decision procedures for classical modal logics

This page was built for publication: Deciding Extended Modal Logics by Combining State Space Generation and SAT Solving

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