package coq-smtcoq

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

Install

Dune Dependency

smtcoq.github.io Edit opam file Versions (15)

Authors

  1. M
    Michaël Armand
  2. V
    Valentin Blot
  3. A
    Amina Bousalem
  4. B
    Boris Djalal
  5. L
    Louise Dubois de Prisque
  6. Q
    Quentin Garchery
  7. B
    Benjamin Grégoire
  8. C
    Chantal Keller
  9. B
    Burak Ekici
  10. A
    Alain Mebsout

Maintainers

  1. C
    ckeller@lmf.cnrs.fr

Sources

SMTCoq-2.3+8.20.tar.gz
sha512=b03a6fcf5ae29b2bf241321a695d41fc7d0ede079e40b32bc20b45814e066ad046257dbaba011675706060c3c75461f08a06607d401d7078ce1d06f51bf9e9c0

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
  • abducts for goals that external solvers fail to prove, which represent possibly missing hypotheses that would allow them to prove the goal, using the cvc5 SMT solver.

Tags

category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword: SMT keyword: SAT keyword: automation logpath:SMTCoq

Published: 19 Sep 2024

Dependencies (3)

  1. coq >= "8.20~" & < "8.21~"
  2. num
  3. ocaml >= "4.07.1"

Dev Dependencies

None

Used by (1)

  1. coq-sniper

Conflicts

None