<div class="csl-bib-body">
<div class="csl-entry">Eisenhofer, C., Kovács, L., & Rawson, M. (2024). Embedding the Connection Calculus in Satisfiability Modulo Theories. In <i>Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023)</i> (pp. 54–63). CEUR-WS.org. https://doi.org/10.34726/5394</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/192933
-
dc.identifier.uri
https://doi.org/10.34726/5394
-
dc.description.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
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
CEUR Workshop Proceedings
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
Connection Calculus
en
dc.subject
Sequent Calculus
en
dc.subject
SMT
en
dc.subject
User-Propagation
en
dc.subject
Deduction System
en
dc.title
Embedding the Connection Calculus in Satisfiability Modulo Theories
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34726/5394
-
dc.description.startpage
54
-
dc.description.endpage
63
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.relation.grantno
F 85
-
dc.relation.grantno
ICT22-007
-
dc.rights.holder
2023 The Authors
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1613-0073
-
tuw.booktitle
Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023)
-
tuw.container.volume
3613
-
tuw.peerreviewed
true
-
tuw.book.ispartofseries
CEUR Workshop Proceedings
-
tuw.relation.publisher
CEUR-WS.org
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.project.title
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design
-
tuw.project.title
Effective Formal Methods for Smart-Contract Certification
-
tuw.researchTopic.id
C4
-
tuw.researchTopic.id
C5
-
tuw.researchTopic.name
Mathematical and Algorithmic Foundations
-
tuw.researchTopic.name
Computer Science Foundations
-
tuw.researchTopic.value
50
-
tuw.researchTopic.value
50
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
dc.identifier.libraryid
AC17203991
-
dc.description.numberOfPages
10
-
tuw.author.orcid
0000-0003-0339-1580
-
tuw.author.orcid
0000-0002-8299-2714
-
tuw.author.orcid
0000-0001-7834-1567
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
tuw.event.name
1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023)
en
tuw.event.startdate
18-09-2023
-
tuw.event.enddate
18-09-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Prag
-
tuw.event.country
CZ
-
tuw.event.institution
CTU
-
tuw.event.presenter
Eisenhofer, Clemens
-
tuw.event.track
Single Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.grantfulltext
open
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openaccessfulltext
Open Access
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192 - Institut für Logic and Computation
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.orcid
0000-0003-0339-1580
-
crisitem.author.orcid
0000-0002-8299-2714
-
crisitem.author.orcid
0000-0001-7834-1567
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E180 - Fakultät für Informatik
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
FWF - Österr. Wissenschaftsfonds
-
crisitem.project.funder
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
