<div class="csl-bib-body">
<div class="csl-entry">Kaufmann, D., & Hofstadler, C. (2025). Recycling Algebraic Proof Certificates. In M. Erașcu & M. Janota (Eds.), <i>Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC-Square 2025) Collocated with The 30th International Conference on Automated Deduction (CADE 2025)</i> (pp. 35–40). CEUR-WS.org. http://hdl.handle.net/20.500.12708/222940</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/222940
-
dc.description.abstract
Proof certificates can be used to validate the correctness of algebraic derivations. However, in practice, we frequently observed that the exact same proof steps are repeated for different sets of variables, which leads to unnecessarily large proofs. To overcome this issue we extend the existing Practical Algebraic Calculus with linear combinations (LPAC) with two new proof rules that allow us to capture and reuse parts of the proof to derive a more condensed proof certificate. We integrate these rules into the proof checker Pacheck 2.0. Our experimental
results demonstrate that the proposed extension helps to reduce both proof size and verification time.
en
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
CEUR Workshop Proceedings
-
dc.subject
Proof Logging
en
dc.subject
Algebraic Calculus
en
dc.subject
Recycling Proofs
en
dc.title
Recycling Algebraic Proof Certificates
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.affiliation
Johannes Kepler University of Linz, Austria
-
dc.contributor.editoraffiliation
West University of Timişoara, Romania
-
dc.contributor.editoraffiliation
Czech Technical University in Prague, Czechia
-
dc.description.startpage
35
-
dc.description.endpage
40
-
dc.relation.grantno
ESP 666-N
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1613-0073
-
tuw.booktitle
Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC-Square 2025) Collocated with The 30th International Conference on Automated Deduction (CADE 2025)
-
tuw.container.volume
4116
-
tuw.peerreviewed
true
-
tuw.relation.publisher
CEUR-WS.org
-
tuw.project.title
Wortbasiertes Reasoning mit Computeralgebra und SAT
-
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
-
dc.description.numberOfPages
6
-
tuw.author.orcid
0000-0002-3025-0604
-
tuw.editor.orcid
0000-0003-3487-784X
-
tuw.event.name
the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC-Square 2025)
en
tuw.event.startdate
02-08-2025
-
tuw.event.enddate
02-08-2025
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Stuttgart
-
tuw.event.country
DE
-
tuw.event.presenter
Kaufmann, Daniela
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openairetype
conference paper
-
item.fulltext
no Fulltext
-
item.grantfulltext
none
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
