Embedding the Connection Calculus in Satisfiability Modulo Theories

Eisenhofer, Clemens; Kovács, Laura; Rawson, Michael

doi:10.34726/5394

Record link:

http://hdl.handle.net/20.500.12708/192933
https://doi.org/10.34726/5394

Title:

Embedding the Connection Calculus in Satisfiability Modulo Theories

Citation:

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

reposiTUm DOI:

10.34726/5394

CatalogPlus:

AC17203991

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Eisenhofer, Clemens
Kovács, Laura
Rawson, Michael

Organisational Unit:

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)

Event date:

18-Sep-2023

Event place:

Prag, Czechia

Number of Pages:

Publisher:

CEUR-WS.org

Peer reviewed:

Yes

Keywords:

Connection Calculus; Sequent Calculus; SMT; User-Propagation; Deduction System

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.

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%

Science Branch:

1020 - Informatik: 100%

License:

CC BY 4.0