nunchaku

A counter-example finder for higher-order logic.
Description

Nunchaku is a counter-example finder for higher-order logic, designed to be used from various proof assistants, and a spiritual successor to Nitpick. It relies encodings and external solvers (CVC4, kodkod, paradox, smbc) to find models, thanks to its modular architecture.

Install
Published
29 Aug 2017
Authors
Maintainers
Sources
0.5.tar.gz
md5=66a16f7d6fdbbb688a479e4cf3354f99
Dependencies
oasis build
menhir build & <= "20181026"
containers >= "1.0"
ocaml >= "4.01.0" & < "4.06.0"
Reverse Dependencies