Non-classical logics in satisfiability modulo theories

DOI10.1007/978-3-031-43513-3_2MaRDI QIDQ6541143zbMATH OpenFDO

Authors Clemens Eisenhofer, Michael G. Rawson, Laura Kovács

Publication date 17 May 2024

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

non-classical logicsSMTtableauxuser-propagators

Mathematics Subject Classification ID

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

Cites work

• scientific article; zbMATH DE number 4219104 (Why is no real title available?)
• scientific article; zbMATH DE number 1405450 (Why is no real title available?)
• scientific article; zbMATH DE number 7592011 (Why is no real title available?)
• A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
• An efficient SMT solver for string constraints
• An introduction to description logic
• Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs
• Automated reasoning in \(\mathcal{ALCQ}\) via SMT
• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Foundations of Information and Knowledge Systems
• From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain
• Implementing tableau calculi using BDDs: BDDTab system description
• Local reductions for the modal cube
• Modal Satisfiability via SMT Solving
• Reasoning with finite sets and cardinality constraints in SMT
• SAT modulo intuitionistic implications
• Tableau methods of proof for modal logics
• The MET: The Art of Flexible Reasoning with Modalities
• The axiomatic translation principle for modal logic
• Theorem provers for every normal modal logic

This page was built for publication: Non-classical logics in satisfiability modulo theories

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