Eisenhofer, C., Kovács, L., & Rawson, M. (2024). Embedding the Connection Calculus in Satisfiability Modulo Theories. In Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) (pp. 54–63). CEUR-WS.org. https://doi.org/10.34726/5394
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Erschienen in:
Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023)
-
Band:
3613
-
Datum (veröffentlicht):
Jan-2024
-
Veranstaltungsname:
1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023)
en
Veranstaltungszeitraum:
18-Sep-2023
-
Veranstaltungsort:
Prag, Tschechien
-
Umfang:
10
-
Verlag:
CEUR-WS.org
-
Peer Reviewed:
Ja
-
Keywords:
Connection Calculus; Sequent Calculus; SMT; User-Propagation; Deduction System
en
Abstract:
We investigate embedding a broad class of deduction systems in satisfiability solvers such as Z3. One such deduction system is the connection calculus. Using Z3’s support for user-propagation, proofs in a user-specified calculus can be found automatically via Z3’s internal satisfiability procedures. The approach places few constraints on the deduction system, yet allows for domain-specific optimisations if known. We discuss ramifications for proof search in the connection calculus.
en
Projekttitel:
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) Effective Formal Methods for Smart-Contract Certification: ICT22-007 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
-
Forschungsschwerpunkte:
Mathematical and Algorithmic Foundations: 50% Computer Science Foundations: 50%
CC BY 4.0
