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
-
Published in:
Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023)
-
Volume:
3613
-
Date (published):
Jan-2024
-
Event name:
1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023)
en
Event date:
18-Sep-2023
-
Event place:
Prag, Czechia
-
Number of Pages:
10
-
Publisher:
CEUR-WS.org
-
Peer reviewed:
Yes
-
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
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) Effective Formal Methods for Smart-Contract Certification: ICT22-007 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
-
Research Areas:
Mathematical and Algorithmic Foundations: 50% Computer Science Foundations: 50%
CC BY 4.0
