Fast and flexible proof checking for SMT
Duckki Oe, Andrew J. Reynolds, Aaron Stump · 2009
Fast and flexible proof checking can be implemented for SMT using the Edinburgh Logical Framework with Side Conditions (LFSC). LFSC provides a declarative format for describing proof systems as signatures. We describe several optimizations for LFSC proof checking, and report experiments on QF_IDL benchmarks showing proof-checking overhead of 32% of the solving time required by our clsat solver.