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.12.tar.gz
sha512=07a602bd62ffa1226802248b47ee076f81f5f99148b2f5b5908c09b1cdd100d0369de436b05b58aa7a5607d7525f8d05441b6fa7d88c03c37caf1e66515b4d1c

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

Dev Dependencies

None

Used by (1)

  1. coq-sniper

Conflicts

None

Rocq

Interactive Theorem Prover