diff -r f353fe3c2b92 -r 6c38df1d294a src/HOL/TPTP/CASC/SysDesc_Nitpick.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/CASC/SysDesc_Nitpick.html Tue May 21 11:01:14 2013 +0200
@@ -0,0 +1,82 @@
+
+Nitpick 2013
+Jasmin C. Blanchette
+Technische Universität München, Germany
+
+Architecture
+
+Nitpick [BN10] is an open source counterexample
+generator for Isabelle/HOL [NPW13]. It builds on
+Kodkod [TJ07], a highly optimized first-order
+relational model finder based on SAT. The name Nitpick is appropriated from a
+now retired Alloy precursor. In a case study, it was applied successfully to a
+formalization of the C++ memory model [BWB+11].
+
+Strategies
+
+
+Nitpick employs Kodkod to find a finite model of the negated conjecture. The
+translation from HOL to Kodkod's first-order relational logic (FORL) is
+parameterized by the cardinalities of the atomic types occurring in it. Nitpick
+enumerates the possible cardinalities for each atomic type, exploiting
+monotonicity to prune the search space [BK11]. If a
+formula has a finite counterexample, the tool eventually finds it, unless it
+runs out of resources.
+
+
+SAT solvers are particularly sensitive to the encoding of problems, so special
+care is needed when translating HOL formulas.
+As a rule, HOL scalars are mapped to FORL singletons and functions are mapped to
+FORL relations accompanied by a constraint. More specifically,
+an n-ary first-order function (curried or not) can be coded as an
+(n + 1)-ary relation accompanied by a constraint. However, if the return
+type is the type of Booleans, the function is more efficiently coded as an
+unconstrained n-ary relation.
+Higher-order quantification and functions bring complications of their own. A
+function from σ to τ cannot be directly passed as an argument in FORL;
+Nitpick's workaround is to pass |σ| arguments of type τ that encode a
+function table.
+
+
Implementation
+
+
+Nitpick, like most of Isabelle/HOL, is written in Standard ML. Unlike Isabelle
+itself, which adheres to the LCF small-kernel discipline, Nitpick does not
+certify its results and must be trusted.
+
+Nitpick is available as part of Isabelle/HOL for all major platforms under a
+BSD-style license from
+
+ http://www.cl.cam.ac.uk/research/hvg/Isabelle
+
+Expected Competition Performance
+
+Thanks to Kodkod's amazing power, we expect that Nitpick will beat both Satallax
+and Refute with its hands tied behind its back in the TNT category.
+
+References
+
+- BK11
+
- Blanchette J. C., Krauss A. (2011),
+ Monotonicity Inference for Higher-Order Formulas,
+ J. Autom. Reasoning 47(4), pp. 369–398, 2011.
+
- BN10
+
- Blanchette J. C., Nipkow T. (2010),
+ Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder,
+ ITP 2010, LNCS 6172, pp. 131–146, Springer.
+
- BWB+11
+
- Blanchette J. C., Weber T., Batty M., Owens S., Sarkar S. (2011),
+ Nitpicking C++ Concurrency,
+ PPDP 2011, pp. 113–124, ACM Press.
+
- NPW13
+
- Nipkow T., Paulson L. C., Wenzel M. (2013),
+ Isabelle/HOL: A Proof Assistant for Higher-Order Logic,
+ http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf.
+
- TJ07
+
- Torlak E., Jackson D. (2007),
+ Kodkod: A Relational Model Finder, TACAS 2007,
+ LNCS 4424, pp. 632–647, Springer.
+
+
+
+