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
Documentation failed to build. github.com Edit opam file
Published
29 Aug 2017
Authors
Maintainers
Sources
0.5.tar.gz
md5=66a16f7d6fdbbb688a479e4cf3354f99
Dependencies
ocamlbuild build
oasis build
num
base-threads
base-unix
sequence
menhir build & <= "20181026"
containers >= "1.0"
ocamlfind build
ocaml >= "4.01.0" & < "4.06.0"
Reverse Dependencies