<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.</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.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.relation.issn
1613-0073
-
dc.description.startpage
35
-
dc.description.endpage
40
-
dc.relation.grantno
ESP 666-N
-
dc.type.category
Full-Paper Contribution
-
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
-
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.openairetype
conference paper
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.grantfulltext
none
-
item.fulltext
no Fulltext
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering