Paper Info
Title
The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
Abstract
Generating and checking proof certificates is important to increase the trust in automated reasoning tools. In recent years formal verification using computer algebra became more important and is heavily used in automated circuit verification. An existing proof format which covers algebraic reasoning and allows efficient proof checking is the practical algebraic calculus. In this paper we present two independent proof checkers PACHECK and PASTÈQUE.The checker Pacheckchecks algebraic proofs more efficiently than PASTÈQUE, but the latter is formally verified using the proof assistant Isabelle/HOL. Furthermore, we introduce extension rules to simulate essential rewriting techniques required in practice. For efficiency we also make use of indices for existing polynomials and include deletion rules too.
Year
DOI
Venue
2020
10.34727/2020/isbn.978-3-85448-042-6_34
2020 Formal Methods in Computer Aided Design (FMCAD)
Keywords
DocType
ISSN
computer algebra,automated circuit verification,existing proof,algebraic reasoning,efficient proof checking,practical algebraic calculus,independent proof checkers PACHECK,PASTÈQUE.The,checker Pacheckchecks algebraic proofs,checking proof certificates,automated reasoning tools,recent years formal verification
Conference
2641-8177
ISBN
Citations 
PageRank 
978-1-7281-5633-0
0
0.34
References 
Authors
20
3
Name
Order
Citations
PageRank
Daniela Kaufmann100.68
mathias fleury2134.95
Armin Biere34106245.11