Proof Checking Technology for Satisfiability Modulo Theories

Citations of this article
Mendeley users who have this article in their library.


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.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free