<div class="csl-bib-body">
<div class="csl-entry">Rawson, M., Eisenhofer, C., & Kovács, L. (2026). Constraint Learning for Non-confluent Proof Search. In <i>Automated Reasoning with Analytic Tableaux and Related Methods</i> (pp. 103–119). Springer Cham. https://doi.org/10.1007/978-3-032-06085-3_6</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/226882
-
dc.description.abstract
Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt constraint learning to reduce backtracking in the classical first-order connection calculus, while retaining completeness. An initial constraint learning language for connection-driven search is iteratively refined to greatly reduce backtracking in practice. The approach may be useful for proof search in other non-confluent tableau calculi.
en
dc.description.sponsorship
European Commission
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.subject
Backjumping
en
dc.subject
Connection Tableaux
en
dc.subject
Constraint Learning
en
dc.title
Constraint Learning for Non-confluent Proof Search
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.relation.isbn
978-3-032-06085-3
-
dc.relation.doi
10.1007/978-3-032-06085-3
-
dc.relation.issn
0302-9743
-
dc.description.startpage
103
-
dc.description.endpage
119
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
Automated Reasoning with Analytic Tableaux and Related Methods
-
tuw.container.volume
15980
-
tuw.peerreviewed
true
-
tuw.relation.publisher
Springer Cham
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publication.orgunit
E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies
-
tuw.publication.orgunit
E056-13 - Fachbereich LogiCS
-
tuw.publication.orgunit
E056-17 - Fachbereich Trustworthy Autonomous Cyber-Physical Systems
-
tuw.publication.orgunit
E056-26 - Fachbereich Automated Reasoning
-
tuw.publisher.doi
10.1007/978-3-032-06085-3_6
-
dc.description.numberOfPages
17
-
tuw.author.orcid
0000-0001-7834-1567
-
tuw.author.orcid
0000-0003-0339-1580
-
tuw.author.orcid
0000-0002-8299-2714
-
tuw.event.name
TABLEAUX 2025: 34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
en
tuw.event.startdate
27-09-2025
-
tuw.event.enddate
29-09-2025
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Reykjavik
-
tuw.event.country
IS
-
tuw.event.presenter
Eisenhofer, Clemens
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.grantfulltext
none
-
item.cerifentitytype
Publications
-
item.openairetype
conference paper
-
item.languageiso639-1
en
-
item.fulltext
no Fulltext
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
