PV1 ⊧ SMTCoqimports other solvers' proof witnesses and certificates to Coq

Plug-in for the integration of external solvers into the Coq proof assistant

Application domain/field

• Proof assistants
• SMT solvers
• SAT solvers
• Proof certificates

Type of tool

Metatool

Internals

SMTCoq is a plugin for the Coq proof assistant. It allows users to use external solvers (SAT or SMT) inside Coq. If these solvers succeed in proving a goal and return a proof witness or certificate, SMTCoq can use this to reconstruct a proof of the goal within Coq automatically. Uses CVC4, zChaff, veriT. SMTCoq is also available as an opam package.