Proof logging for computer algebra based SMT solving

In formal verification, proof logging is a technique for automatically reviewing the reasoning steps of a proof engine by a separate tool. This is useful for enhancing the confidence in the prover´s result, especially in the case of a positive answer when no counterexample exists. Mature proof logging techniques exist for single-theory provers. SMT solvers, however, combine several theories so that developing an unified proof logging technique is more challenging. This paper proposes an approach for logging the proofs of the SMT solver STABLE which is a prover combining SAT and computer algebra engines. We show how to translate the SAT proofs into algebraic forms (polynomials) and how to check the combined Boolean and word-level proofs using a separate computer algebra engine.