Modal Satisfiability via SMT Solving

DOI10.1007/978-3-319-15545-6_5zbMath1453.03015OpenAlexW2110715144MaRDI QIDQ5256336

Stephan Merz, Carlos Areces, Pascal Fontaine

Publication date: 22 June 2015

Published in: Software, Services, and Systems (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01127966/file/main.pdf

Mathematics Subject Classification ID

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

Related Items (1)

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modal languages and bounded fragments of predicate logic
• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• Solving SAT and SAT Modulo Theories
• Using the Universal Modality: Gains and Questions
• On the Decision Problem for Two-Variable First-Order Logic
• Functional translation and second-order frame properties of modal logics
• Resolution-based methods for modal logics
• First-Order Resolution Methods for Modal Logics
• Using tableau to decide description logics with full role negation and identity
• Termination for Hybrid Tableaus
• On Computable Numbers, with an Application to the Entscheidungsproblem

This page was built for publication: Modal Satisfiability via SMT Solving