Kaufmann Daniela, Fleury Mathias, Biere Armin, Kauers Manuel
Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria.
Chair of Computer Architecture, Albert-Ludwigs-University, Freiburg, Germany.
Form Methods Syst Des. 2024;64(1-3):73-107. doi: 10.1007/s10703-022-00391-x. Epub 2022 Apr 11.
Automated reasoning techniques based on computer algebra have seen renewed interest in recent years and are for example heavily used in formal verification of arithmetic circuits. However, the verification process might contain errors. Generating and checking proof certificates is important to increase the trust in automated reasoning tools. For algebraic reasoning, two proof systems, Nullstellensatz and polynomial calculus, are available and are well-known in proof complexity. A Nullstellensatz proof captures whether a polynomial can be represented as a linear combination of a given set of polynomials by providing the co-factors of the linear combination. Proofs in polynomial calculus dynamically capture that a polynomial can be derived from a given set of polynomials using algebraic ideal theory. In this article we present the practical algebraic calculus as an instantiation of the polynomial calculus that can be checked efficiently. We further modify the practical algebraic calculus and gain LPAC (practical algebraic calculus + linear combinations) that includes linear combinations. In this way we are not only able to represent both Nullstellensatz and polynomial calculus proofs, but we are also able to blend both proof formats. 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. We demonstrate the different proof formats on the use case of arithmetic circuit verification and discuss how these proofs can be produced as a by-product in formal verification. We present the proof checkers Pacheck, Pastèque, and Nuss-Checker. Pacheck checks proofs in practical algebraic calculus more efficiently than Pastèque, but the latter is formally verified using the proof assistant Isabelle/HOL. The tool Nuss-Checker is used to check proofs in the Nullstellensatz format.
The online version contains supplementary material available at 10.1007/s10703-022-00391-x.
近年来，基于计算机代数的自动推理技术重新受到关注，例如在算术电路的形式验证中被大量使用。然而，验证过程可能包含错误。生成和检查证明证书对于提高对自动推理工具的信任很重要。对于代数推理，有两种证明系统，即零点定理和多项式演算，它们在证明复杂性方面是众所周知的。零点定理证明通过提供线性组合的余因子来捕捉一个多项式是否可以表示为给定多项式集的线性组合。多项式演算中的证明使用代数理想理论动态捕捉一个多项式可以从给定的多项式集中推导出来。在本文中，我们提出了实用代数演算作为多项式演算的一种实例化，它可以被高效地检查。我们进一步修改了实用代数演算，并获得了包括线性组合的LPAC（实用代数演算+线性组合）。通过这种方式，我们不仅能够表示零点定理和多项式演算证明，还能够融合这两种证明格式。此外，我们引入扩展规则来模拟实际中所需的基本重写技术。为了提高效率，我们还对现有多项式使用索引，并包括删除规则。我们在算术电路验证的用例上展示了不同的证明格式，并讨论了如何在形式验证中作为副产品生成这些证明。我们展示了证明检查器Pacheck、Pastèque和Nuss-Checker。Pacheck比Pastèque更高效地检查实用代数演算中的证明，但后者是使用证明助手Isabelle/HOL进行形式验证的。工具Nuss-Checker用于检查零点定理格式的证明。
在线版本包含可在10.1007/s10703-022-00391-x获取的补充材料。
