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.13.tar.gz
sha512=5909679b27b67ccca4265e07551d69aedbb3c320b7a3c1eea9dc9d6d2f82c54fc4710f8dfd7bf9f205bcf15f5c62b9391d3e36e7d37048f0dcb97df9c9281168

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.13~" & < "8.14~"
  2. ocaml >= "4.07.1"

Dev Dependencies

None

Used by (1)

  1. coq-sniper

Conflicts

None

Rocq

Interactive Theorem Prover