<div class="csl-bib-body">
<div class="csl-entry">Eisenhofer, C., Alassaf, R., Rawson, M., & Kovács, L. (2023). Non-Classical Logics in Satisfiability Modulo Theories. In D. R. S. Ramanayake & J. Urban (Eds.), <i>Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings</i> (pp. 24–36). Springer. https://doi.org/10.1007/978-3-031-43513-3_2</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/190634
-
dc.description.abstract
We show that tableau methods for satisfiability in non-classical logics can be supported naturally in SMT solving via the framework of user-propagators. By way of demonstration, we implement the description logic $$\mathcal {ALC}$$ in the Z3 SMT solver and show that working with user-propagators allows us to significantly outperform encodings to first-order logic with relatively little effort. We promote user-propagators for creating solvers for non-classical logics based on tableau calculi.
en
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
Non-Classical Logics
en
dc.subject
SMT
en
dc.subject
Tableaux
en
dc.subject
User-Propagators
en
dc.title
Non-Classical Logics 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.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.editoraffiliation
Czech Technical University in Prague, Czechia
-
dc.relation.isbn
978-3-031-43513-3
-
dc.relation.doi
10.1007/978-3-031-43513-3
-
dc.relation.issn
0302-9743
-
dc.description.startpage
24
-
dc.description.endpage
36
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.relation.grantno
F 85
-
dc.rights.holder
The Author(s) 2023
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
dc.publisher.place
Cham
-
tuw.booktitle
Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings
-
tuw.container.volume
14278
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
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.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
-
tuw.publisher.doi
10.1007/978-3-031-43513-3_2
-
dc.identifier.libraryid
AC17202025
-
dc.description.numberOfPages
13
-
tuw.author.orcid
0000-0003-0339-1580
-
tuw.author.orcid
0000-0002-0331-2451
-
tuw.author.orcid
0000-0001-7834-1567
-
tuw.author.orcid
0000-0002-8299-2714
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
tuw.editor.orcid
0000-0002-7940-9065
-
tuw.event.name
32nd Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023)
en
tuw.event.startdate
18-09-2023
-
tuw.event.enddate
21-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
Czech Technical University in Prague
-
tuw.event.presenter
Eisenhofer, Clemens
-
tuw.event.track
Single Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.grantfulltext
open
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openaccessfulltext
Open Access
-
item.openairetype
conference paper
-
item.cerifentitytype
Publications
-
item.fulltext
with Fulltext
-
item.mimetype
application/pdf
-
item.languageiso639-1
en
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
University of Manchester
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
