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

DOI10.1007/978-3-319-99957-9_8zbMath1515.68348MaRDI QIDQ6108819

Martin Strecker

Publication date: 30 June 2023

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

zbMATH Keywords

modal logicautomated theorem provinggraph transformationsprogram verification

Mathematics Subject Classification ID

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

Cites Work

• SAT-based decision procedures for classical modal logics
• Revisiting enumerative instantiation
• A Hoare-Like Calculus Using the SROIQ σ Logic on Transformations of Graphs
• Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability
• Automated Reasoning in $\mathcal{ALCQ}$ via SMT
• Modal Satisfiability via SMT Solving

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