package coq-smtcoq
A Coq plugin that checks proof witnesses coming from external SAT and SMT solvers
Install
Dune Dependency
Authors
Maintainers
Sources
SMTCoq-2.2+8.16.tar.gz
sha512=bff6ab19c7850beff8f2a11e6db847b9e5910c86dc76d3cca66fd22088e3bac8d7bc751ba1e3e731f9b52282873d10e793fbd0e38241b1d24e476356bc2c2e71
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:SMTCoqPublished: 31 Jan 2024
Dev Dependencies
None
Used by (1)
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page