Sciweavers

ITP
2010
164views Mathematics» more  ITP 2010»
13 years 8 months ago
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification, (co)ind...
Jasmin Christian Blanchette, Tobias Nipkow