<div class="csl-bib-body">
<div class="csl-entry">Hajdu, M., Kovács, L., & Voronkov, A. (2025). Partial Redundancy in Saturation. In C. Barrett & U. Waldmann (Eds.), <i>Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings</i> (pp. 532–551). https://doi.org/10.1007/978-3-031-99984-0_28</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/221536
-
dc.description.abstract
Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We strengthen redundancy elimination by introducing a new notion of redundancy, based on partial clauses and redundancy formulas. The new notion allows us to recognize redundant clauses and inferences that cannot be recognized by standard redundancy elimination criteria. In a way, our notion blurs the distinction between redundancy at the level of inferences and redundancy at the level of clauses. We present a superposition calculus PaRC on partial clauses and prove that it is refutationally complete. We discuss the implementation of the calculus in the theorem prover Vampire. Our experiments show the power of the new approach: we were able to solve 24 TPTP problems not previously solved by any prover, including previous versions of Vampire.
en
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
Amazon Research Awards
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.subject
saturation-based theorem proving
en
dc.subject
superposition calculus
en
dc.subject
redundancy
en
dc.subject
Vampire
-
dc.title
Partial Redundancy in Saturation
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.editoraffiliation
Stanford University
-
dc.contributor.editoraffiliation
Max Planck Institute for Informatics (Saarbrücken, DE)
-
dc.relation.isbn
978-3-031-99983-3
-
dc.relation.doi
10.1007/978-3-031-99984-0
-
dc.description.startpage
532
-
dc.description.endpage
551
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.relation.grantno
ICT22-007
-
dc.relation.grantno
101213411
-
dc.relation.grantno
ARA 20223
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings
-
tuw.container.volume
15943
-
tuw.peerreviewed
true
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.project.title
Effective Formal Methods for Smart-Contract Certification
-
tuw.project.title
LEARN: Learning Efficient Automated Reasoning on the Net
-
tuw.project.title
QuAT: Quantifiers and Arithmetic Theories are Friends with Benefits
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.id
C5
-
tuw.researchTopic.name
Logic and Computation
-
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-99984-0_28
-
dc.description.numberOfPages
20
-
tuw.author.orcid
0000-0002-8273-2613
-
tuw.author.orcid
0000-0002-8299-2714
-
tuw.editor.orcid
0000-0002-0676-7195
-
tuw.event.name
30th International Conference on Automated Deduction
en
dc.description.sponsorshipexternal
TU Wien Doctoral College SecInt
-
tuw.event.startdate
28-07-2025
-
tuw.event.enddate
31-07-2025
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Stuttgart
-
tuw.event.country
DE
-
tuw.event.presenter
Hajdu, Marton
-
tuw.event.track
Single Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.cerifentitytype
Publications
-
item.openairetype
conference paper
-
item.fulltext
no Fulltext
-
item.languageiso639-1
en
-
item.grantfulltext
none
-
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
-
crisitem.author.orcid
0000-0002-8273-2613
-
crisitem.author.orcid
0000-0002-8299-2714
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
