Datensatz Zitierlink: 
http://hdl.handle.net/20.500.12708/192933
https://doi.org/10.34726/5394
-
Titel: 
Embedding the Connection Calculus in Satisfiability Modulo Theories
en
Zitat: 
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
-
Publikationstyp: 
Konferenzbeitrag - Full-Paper Contribution
de
Sprache: 
Englisch
-
Autor_innen: 
Eisenhofer, Clemens 
Kovács, Laura 
Rawson, Michael 
-
Organisations­einheit: 
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
-
Veranstaltungs­name: 
1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) 
en
Veranstaltungs­zeitraum: 
18-Sep-2023
-
Veranstaltungs­ort: 
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) 
-
Forschungs­schwerpunkte: 
Mathematical and Algorithmic Foundations: 50%
Computer Science Foundations: 50%
-
Wissenschafts­zweig: 
1020 - Informatik: 100%
-
Lizenz: 
CC BY 4.0 CC BY 4.0
en
Enthalten in den Sammlungen:
Conference Paper

Miniaturbild
Volltext (Version of Record (published version))
Adobe PDF
(248.21 kB)
Open Access CC BY 4.0
Zur Langanzeige

Google ScholarTM

Check