package coq-smtcoq

You can search for identifiers within the package.

in-package search v0.2.0

A Coq plugin that checks proof witnesses coming from external SAT and SMT solvers

Install

sha512=fce92b7c22ff453055c69666980b1f285fd5a9819fb741b206cacf311d1762030d0c25e7235d7d56888da84ac00384ae760f1111321c82249c47f3ca3b9a88b8

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.

None

None

On This Page