A common proof format for solvers for Satisfiability Modulo Theories (SMT) is proposed, based on the Edinburgh Logical Framework (LF). Two problems arise: checking very large proofs, and keeping proofs compact in the presence of complex side conditions on rules. Incremental checking combines parsing and proof checking in a single step, to avoid building in-memory representations of proof subterms. LF with Side Conditions (LFSC) extends LF to allow side conditions to be expressed using a simple first-order functional programming language. Experimental data with an implementation show very good proof checking times and memory usage on benchmarks including the important example of resolution inferences. © 2008 Elsevier B.V. All rights reserved.
Stump, A. (2009). Proof Checking Technology for Satisfiability Modulo Theories. Electronic Notes in Theoretical Computer Science, 228(C), 121–133. https://doi.org/10.1016/j.entcs.2008.12.121