added CASC-related files, to keep a public record of the Isabelle submission at the competition
<HR><!------------------------------------------------------------------------><H2>Nitrox 2013</H2>Jasmin C. Blanchette<sup>1</sup>, Emina Torlak<sup>2</sup><BR><sup>1</sup>Technische Universität München, Germany <BR><sup>2</sup>University of California, Berkeley, USA <BR><H3>Architecture</H3>Nitrox is the first-order version of Nitpick [<A HREF="#References">BN10</A>],an open source counterexample generator for Isabelle/HOL[<A HREF="#References">NPW13</A>]. It builds on Kodkod[<A HREF="#References">TJ07</A>], a highly optimized first-order relationalmodel finder based on SAT. The name Nitrox is a portmanteau of <b><i>Nit</i></b>pickand Pa<b><i>r</i></b>ad<b><i>ox</i></b> (clever, eh?).<H3>Strategies</H3><p>Nitrox employs Kodkod to find a finite model of the negated conjecture. Itperforms a few transformations on the input, such as pushing quantifiers inside,but 99% of the solving logic is in Kodkod and the underlying SAT solver.<p>The translation from HOL to Kodkod's first-order relational logic (FORL) isparameterized by the cardinalities of the atomic types occurring in it. Nitroxenumerates the possible cardinalities for the universe. If a formula has afinite counterexample, the tool eventually finds it, unless it runs out ofresources.<p>Nitpick is optimized to work with higher-order logic (HOL) and its definitionalprinciples (e.g., (co)inductive predicates, (co)inductive datatypes,(co)recursive functions). When invoked on untyped first-order problem, few ofits optimizations come into play, and the problem handed to Kodkod isessentially a first-order relational logic (FORL) rendering of the TPTP FOFproblem. There are two main exceptions:<ul><li> Nested quantifiers are moved as far inside the formula as possible beforeKodkod gets a chance to look at them [<A HREF="#References">BN10</A>].<li> Definitions invoked with fixed arguments are specialized.</ul><H3>Implementation</H3><p>Nitrox, like most of Isabelle/HOL, is written in Standard ML. Unlike Isabelleitself, which adheres to the LCF small-kernel discipline, Nitrox does notcertify its results and must be trusted. Kodkod is written in Java. MiniSat 1.14is used as the SAT solver.<H3>Expected Competition Performance</H3>Since Nitpick was designed for HOL, it doesn't have any type inference àla Paradox. It also doesn't use the SAT solver incrementally, which penalizes ita bit (but not as much as the missing type inference). Kodkod itself is known toperform less well on FOF than Paradox, because it is designed and optimized fora somewhat different logic, FORL. On the other hand, Kodkod's symmetry breakingmight be better calibrated than Paradox's. Hence, we expect Nitrox to end up insecond or third place in the FNT category.<H3>References</H3><DL><DT> BN10<DD> Blanchette J. C., Nipkow T. (2010), <STRONG>Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder</STRONG>, ITP 2010, <EM>LNCS</EM> 6172, pp. 131–146, Springer.<DT> NPW13<DD> Nipkow T., Paulson L. C., Wenzel M. (2013), <STRONG>Isabelle/HOL: A Proof Assistant for Higher-Order Logic</STRONG>, <A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf">http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf</a>.<DT> TJ07<DD> Torlak E., Jackson D. (2007), <STRONG>Kodkod: A Relational Model Finder</STRONG>, TACAS 2007, <EM>LNCS</EM> 4424, pp. 632–647, Springer.</DL><P><HR><!------------------------------------------------------------------------>