Eisenhofer, C., Alassaf, R., Rawson, M., & Kovács, L. (2023). Non-Classical Logics in Satisfiability Modulo Theories. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 24–36). Springer. https://doi.org/10.1007/978-3-031-43513-3_2
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings
We show that tableau methods for satisfiability in non-classical logics can be supported naturally in SMT solving via the framework of user-propagators. By way of demonstration, we implement the description logic $$\mathcal {ALC}$$ in the Z3 SMT solver and show that working with user-propagators allows us to significantly outperform encodings to first-order logic with relatively little effort. We promote user-propagators for creating solvers for non-classical logics based on tableau calculi.
en
Project title:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission) Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 85 (FWF - Österr. Wissenschaftsfonds)
-
Research Areas:
Mathematical and Algorithmic Foundations: 50% Computer Science Foundations: 50%
CC BY 4.0
