Recycling Algebraic Proof Certificates

TL;DR

This paper introduces an extension to algebraic proof certificates that enables proof parts to be reused, significantly reducing proof size and verification time in algebraic derivations.

Contribution

It extends the LPAC calculus with new proof rules for reusing proof segments, integrated into Pacheck 2.0, improving proof efficiency.

Findings

Reduced proof size in algebraic derivations

Decreased verification time with the new proof rules

Effective proof reuse demonstrated in experiments

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.