package coq-smtcoq

  1. Overview
  2. Homepage
A Coq plugin that checks proof witnesses coming from external SAT and SMT solvers

Install

Dune Dependency

Authors

Maintainers

Sources

SMTCoq-2.0+8.11.tar.gz
sha512=21df000ea5eae82073a55fd61090eafd0e265c06e4e772432d22aa4005a39770d968dd5031ebb286c41abb9a9be441f579ead8583b73645f39f111fa1ea928b1

Description

  • a certified checker for proof witnesses coming from the SAT solver ZChaff and the SMT solvers veriT and CVC4. This checker increases the confidence in these tools by checking their answers a posteriori and allows to import new theroems proved by these solvers in Coq;
  • decision procedures through new tactics that discharge some Coq goals to ZChaff, veriT, CVC4, and their combination

Dependencies (2)

  1. coq >= "8.11~" & < "8.12~"
  2. ocaml >= "4.09.0"

Dev Dependencies

None

Used by (1)

  1. coq-sniper

Conflicts

None

Rocq

Interactive Theorem Prover