summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Tue, 21 May 2013 11:01:14 +0200 | |

changeset 52098 | 6c38df1d294a |

parent 52097 | f353fe3c2b92 |

child 52099 | 6225d5b308f9 |

added CASC-related files, to keep a public record of the Isabelle submission at the competition

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/CASC/ReadMe Tue May 21 11:01:14 2013 +0200 @@ -0,0 +1,168 @@ +Isabelle/HOL 2013 at CASC-24 + +Notes to Geoff: + + Once you have open the archive, Isabelle and its tool are ready to go. The + various tools are invoked as follows: + + Isabelle, competition version: + ./bin/isabelle tptp_isabelle %d %s + + Isabelle, demo version: + ./bin/isabelle tptp_isabelle_hot %d %s + + Nitpick and Nitrox: + ./bin/isabelle tptp_nitpick %d %s + + Refute: + ./bin/isabelle tptp_refute %d %s + + Here's an example: + + ./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/SET/SET014^4.p + + The output should look as follows: + + > val it = (): unit + val commit = fn: unit -> bool + Loading theory "Scratch_tptp_isabelle_hot_29414_2568" + running nitpick for 7 s + FAILURE: nitpick + running simp for 15 s + SUCCESS: simp + % SZS status Theorem + + Additional sanity tests: + + ./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/CSR/CSR150^3.p + ./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/SYO/SYO304^5.p + ./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/PUZ/PUZ087^1.p + + The first problem is unprovable; the second one is proved by Satallax; the + third one is proved by LEO-II. + + All the tools accept CNF, FOF, TFF0, or THF0 problems and output SZS statuses + of the form + + % SZS status XXX + + where XXX is in the set + + {Unknown, TimedOut, Unsatisfiable, Theorem, Satisfiable, CounterSatisfiable} + + Nitpick and Nitrox also output a model within "% SZS begin" and "% SZS end" + tags. + + In 2011, there were some problems with Java (needed for Nitpick), because it + required so much memory at startup. I doubt there will be any problems this + year, because Isabelle now includes its own version of Java, but the solution + back then was to replace + + exec "$ISABELLE_TOOL" java + + in the last line of the "contrib/kodkodi-1.5.2/bin/kodkodi" script with + + /usr/lib64/jvm/java-1.5.0-gcj-4.5-1.5.0.0/jre/bin/java + + See the emails we exchanged on July 18, 2011, with the subject "No problem on + my Linux 64-bit". + + Enjoy! + + +Notes to myself: + + I downloaded the official Isabelle2013 Linux package from + + http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013_linux.tar.gz + + on a "macbroy" machine and renamed the directory "Isabelle2013-CASC". I built + a "HOL-TPTP" image: + + ./bin/isabelle build -b HOL-TPTP + + I copied the heaps over to "./heaps": + + mv ~/.isabelle/Isabelle2013/heaps . + + To use this image and suppress some scary output, I added + + HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" + + to the next-to-last lines of "src/HOL/TPTP/lib/Tools/tptp_[inrs]*". + + At this point I tested the "SYN044^4" mentioned above. + + I renamed "README" to "README.orig" and copied this "ReadMe" over. + + Next, I installed and enabled ATPs. + + LEO-II (1.4.3): + + I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved LEO-II from + + http://www.ags.uni-sb.de/~leo/leo2_v1.4.3.tgz + + I did "make opt". I copied + "bin/leo.opt" to "~/Isabelle2013-CASC/contrib/leo". + + I added this line to "etc/settings": + + LEO2_HOME=$ISABELLE_HOME/contrib + + Satallax (2.7): + + I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved Satallax from + + http://www.ps.uni-saarland.de/~cebrown/satallax/downloads/satallax-2.7.tar.gz + + I added E to the path so that it gets detected by Satallax's configure + script: + + export PATH=$PATH:~/Isabelle2013-CASC/contrib/e-1.6-2/x86-linux + + I followed the instructions in "satallax-2.7/INSTALL". I copied + "bin/satallax.opt" to "~/Isabelle2013-CASC/contrib/satallax". + + I added this line to "etc/settings": + + SATALLAX_HOME=$ISABELLE_HOME/contrib + + Vampire (2.6): + + I copied the file "vampire_rel.linux64" from the 2012 CASC archive to + "~/Isabelle2013-CASC/contrib/vampire". + + I added these lines to "etc/settings": + + VAMPIRE_HOME=$ISABELLE_HOME/contrib + VAMPIRE_VERSION=2.6 + + Z3 (3.2): + + I uncommented the following line in "contrib/z3-3.2/etc/settings": + + # Z3_NON_COMMERCIAL="yes" + + To test that the examples actually worked, I did + + ./bin/isabelle tty + theory T imports Main begin; + lemma "a = b ==> [b] = [a]"; + sledgehammer [e leo2 satallax spass vampire z3 z3_tptp] (); + + and I performed the aforementioned sanity tests. + + Ideas for next year: + + * Unfold definitions, esp. if it makes the problem more first-order (cf. + "SEU466^1"). + * Detect and remove needless definitions. + * Expand "p b" to "(b & p True) | (~ b & p False)" (cf. "CSR148^3"). + * Select subset of axioms (cf. "CSR148^3"). + + That's it. + + + Jasmin Blanchette + 21 May 2013

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/CASC/SysDesc_Isabelle.html Tue May 21 11:01:14 2013 +0200 @@ -0,0 +1,183 @@ +<HR><!------------------------------------------------------------------------> +<H2>Isabelle/HOL 2013</H2> +Jasmin C. Blanchette<sup>1</sup>, Lawrence C. Paulson<sup>2</sup>, +Tobias Nipkow<sup>1</sup>, Makarius Wenzel<sup>3</sup> <BR> +<sup>1</sup>Technische Universität München, Germany <BR> +<sup>2</sup>University of Cambridge, United Kingdom <BR> +<sup>3</sup>Université Paris Sud, France <BR> + +<H3>Architecture</H3> + +Isabelle/HOL 2013 [<A HREF="#References">NPW13</A>] is the higher-order +logic incarnation of the generic proof assistant +<A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/">Isabelle2013</A>. +Isabelle/HOL provides several automatic proof tactics, notably an equational +reasoner [<A HREF="#References">Nip89</A>], a classical reasoner [<A +HREF="#References">Pau94</A>], and a tableau prover [<A +HREF="#References">Pau99</A>]. It also integrates external first- and +higher-order provers via its subsystem Sledgehammer [<A +HREF="#References">PB10</A>, <A HREF="#References">BBP11</A>]. + +<P> +Isabelle includes a parser for the TPTP syntaxes CNF, FOF, TFF0, and THF0, due +to Nik Sultana. It also includes TPTP versions of its popular tools, invokable +on the command line as <tt>isabelle tptp_<em>tool</em> <em>max_secs</em> +<em>file.p</em></tt>. For example: + +<blockquote><pre> +isabelle tptp_isabelle_hot 100 SEU/SEU824^3.p +</pre></blockquote> + +<P> +Two versions of Isabelle participate this year. The <em>demo</em> (or HOT) version +includes its competitors LEO-II [<A HREF="#References">BPTF08</A>] and Satallax +[<A HREF="#References">Bro12</A>] as Sledgehammer backends, whereas the +<em>competition</em> version leaves them out. + +<H3>Strategies</H3> + +The <em>Isabelle</em> tactic submitted to the competition simply tries the +following tactics sequentially: + +<DL> +<DT> <tt>sledgehammer</tt> +<DD> Invokes the following sequence of provers as oracles via Sledgehammer: + <UL> + <LI> <tt>satallax</tt>—Satallax 2.4 [<A HREF="#References">Bro12</A>] (<em>demo only</em>); + <LI> <tt>leo2</tt>—LEO-II 1.3.2 [<A HREF="#References">BPTF08</A>] (<em>demo only</em>); + <LI> <tt>spass</tt>—SPASS 3.8ds [<A HREF="#References">BPWW12</A>]; + <LI> <tt>vampire</tt>—Vampire 1.8 (revision 1435) [<A HREF="#References">RV02</A>]; + <LI> <tt>e</tt>—E 1.4 [<A HREF="#References">Sch04</A>]; + <LI> <tt>z3_tptp</tt>—Z3 3.2 with TPTP syntax [<A HREF="#References">dMB08</A>]. + </UL> +<DT> <tt>nitpick</tt> +<DD> For problems involving only the type <tt>$o</tt> of Booleans, checks + whether a finite model exists using Nitpick [<A HREF="#References">BN10</A>]. +<DT> <tt>simp</tt> +<DD> Performs equational reasoning using rewrite rules [<A HREF="#References">Nip89</A>]. +<DT> <tt>blast</tt> +<DD> Searches for a proof using a fast untyped tableau prover and then + attempts to reconstruct the proof using Isabelle tactics + [<A HREF="#References">Pau99</A>]. +<DT> <tt>auto+spass</tt> +<DD> Combines simplification and classical reasoning + [<A HREF="#References">Pau94</A>] under one roof; then invoke Sledgehammer + with SPASS on any subgoals that emerge. +<DT> <tt>z3</tt> +<DD> Invokes the SMT solver Z3 3.2 [<A HREF="#References">dMB08</A>]. +<DT> <tt>cvc3</tt> +<DD> Invokes the SMT solver CVC3 2.2 [<A HREF="#References">BT07</A>]. +<DT> <tt>fast</tt> +<DD> Searches for a proof using sequent-style reasoning, performing a + depth-first search [<A HREF="#References">Pau94</A>]. Unlike + <tt>blast</tt>, it construct proofs directly in Isabelle. That makes it + slower but enables it to work in the presence of the more unusual features + of HOL, such as type classes and function unknowns. +<DT> <tt>best</tt> +<DD> Similar to <tt>fast</tt>, except that it performs a best-first search. +<DT> <tt>force</tt> +<DD> Similar to <tt>auto</tt>, but more exhaustive. +<DT> <tt>meson</tt> +<DD> Implements Loveland's MESON procedure [<A HREF="#References">Lov78</A>]. +Constructs proofs directly in Isabelle. +<DT> <tt>fastforce</tt> +<DD> Combines <tt>fast</tt> and <tt>force</tt>. +</DL> + +<H3>Implementation</H3> + +Isabelle is a generic theorem prover written in Standard ML. Its meta-logic, +Isabelle/Pure, provides an intuitionistic fragment of higher-order logic. The +HOL object logic extends pure with a more elaborate version of higher-order +logic, complete with the familiar connectives and quantifiers. Other object +logics are available, notably FOL (first-order logic) and ZF +(Zermelo–Fraenkel set theory). +<P> +The implementation of Isabelle relies on a small LCF-style kernel, meaning that +inferences are implemented as operations on an abstract <tt>theorem</tt> +datatype. Assuming the kernel is correct, all values of type <tt>theorem</tt> +are correct by construction. +<P> +Most of the code for Isabelle was written by the Isabelle teams at the +University of Cambridge and the Technische Universität München. +Isabelle/HOL is available for all major platforms under a BSD-style license +from +<PRE> + <A HREF="http:////www.cl.cam.ac.uk/research/hvg/Isabelle/">http://www.cl.cam.ac.uk/research/hvg/Isabelle</A></PRE> + +<H3>Expected Competition Performance</H3> + +<P> +Isabelle won last year by a thin margin. This year: first or second place. + +<H3>References</H3> +<DL> + +<DT> BBP11 +<DD> Blanchette J. C., Böhme S., Paulson L. C. (2011), + <STRONG>Extending Sledgehammer with SMT Solvers</STRONG>, + CADE-23, LNAI 6803, pp. 116–130, Springer. +<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> BPTF08 +<DD> Benzmüller C., Paulson L. C., Theiss F., Fietzke A. (2008), + <STRONG>LEO-II—A Cooperative Automatic Theorem Prover for Higher-Order Logic</STRONG>, + IJCAR 2008, <EM>LNAI</EM> 5195, pp. 162–170, Springer. +<DT> BPWW12 +<DD> Blanchette J. C., Popescu A., Wand D., Weidenbach C. (2012), + <STRONG>More SPASS with Isabelle</STRONG>, + ITP 2012, Springer. +<DT> Bro12 +<DD> Brown C. (2012), + <STRONG>Satallax: An Automated Higher-Order Prover (System Description)</STRONG>, + IJCAR 2012, Springer. +<DT> BT07 +<DD> Barrett C., Tinelli C. (2007), + <STRONG>CVC3 (System Description)</STRONG>, + CAV 2007, <EM>LNCS</EM> 4590, pp. 298–302, Springer. +<DT> dMB08 +<DD> de Moura L. M., Bjørner N. (2008), + <STRONG>Z3: An Efficient SMT Solver</STRONG>, + TACAS 2008, <EM>LNCS</EM> 4963, pp. 337–340, Springer. +<DT> Lov78 +<DD> Loveland D. W. (1978), + <STRONG>Automated Theorem Proving: A Logical Basis</STRONG>, + North-Holland Publishing Co. +<DT> Nip89 +<DD> Nipkow T. (1989), + <STRONG>Equational Reasoning in Isabelle</STRONG>, + <EM>Sci. Comput. Program.</EM> 12(2), + pp. 123–149, + Elsevier. +<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> Pau94 +<DD> Paulson L. C. (1994), + <STRONG>Isabelle: A Generic Theorem Prover</STRONG>, + <EM>LNCS</EM> 828, + Springer. +<DT> Pau99 +<DD> Paulson L. C. (1999), + <STRONG>A Generic Tableau Prover and Its Integration with Isabelle</STRONG>, + <EM>J. Univ. Comp. Sci.</EM> 5, + pp. 73–87. +<DT> PB10 +<DD> Paulson L. C., Blanchette J. C. (2010), + <STRONG>Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers</STRONG>, + IWIL-2010. +<DT> RV02 +<DD> Riazanov A., Voronkov A. (2002), + <STRONG>The Design and Implementation of Vampire</STRONG>, + <EM>AI Comm.</EM> 15(2-3), 91–110. +<DT> Sch04 +<DD> Schulz S. (2004), + <STRONG>System Description: E 0.81</STRONG>, + IJCAR 2004, <EM>LNAI</EM> 3097, pp. 223–228, Springer. +</DL> +<P> + +<HR><!------------------------------------------------------------------------>

--- /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 @@ +<HR><!------------------------------------------------------------------------> +<H2>Nitpick 2013</H2> +Jasmin C. Blanchette<BR> +Technische Universität München, Germany <BR> + +<H3>Architecture</H3> + +Nitpick [<A HREF="#References">BN10</A>] is 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 +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 [<A HREF="#References">BWB+11</A>]. + +<H3>Strategies</H3> + +<p> +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 [<A HREF="#References">BK11</A>]. If a +formula has a finite counterexample, the tool eventually finds it, unless it +runs out of resources. + +<p> +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 <i>n</i>-ary first-order function (curried or not) can be coded as an +(<i>n</i> + 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 <i>n</i>-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. + +<H3>Implementation</H3> + +<p> +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. +<P> +Nitpick is available as part of Isabelle/HOL for all major platforms under a +BSD-style license from +<PRE> + <A HREF="http:////www.cl.cam.ac.uk/research/hvg/Isabelle/">http://www.cl.cam.ac.uk/research/hvg/Isabelle</A></PRE> + +<H3>Expected Competition Performance</H3> + +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. + +<H3>References</H3> +<DL> +<DT> BK11 +<DD> Blanchette J. C., Krauss A. (2011), + <STRONG>Monotonicity Inference for Higher-Order Formulas</STRONG>, + <EM>J. Autom. Reasoning</EM> 47(4), pp. 369–398, 2011. +<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> BWB+11 +<DD> Blanchette J. C., Weber T., Batty M., Owens S., Sarkar S. (2011), + <STRONG>Nitpicking C++ Concurrency</STRONG>, + PPDP 2011, pp. 113–124, ACM Press. +<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><!------------------------------------------------------------------------>

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/CASC/SysDesc_Nitrox.html Tue May 21 11:01:14 2013 +0200 @@ -0,0 +1,78 @@ +<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 relational +model finder based on SAT. The name Nitrox is a portmanteau of <b><i>Nit</i></b>pick +and 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. It +performs 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) is +parameterized by the cardinalities of the atomic types occurring in it. Nitrox +enumerates the possible cardinalities for the universe. If a formula has a +finite counterexample, the tool eventually finds it, unless it runs out of +resources. + +<p> +Nitpick is optimized to work with higher-order logic (HOL) and its definitional +principles (e.g., (co)inductive predicates, (co)inductive datatypes, +(co)recursive functions). When invoked on untyped first-order problem, few of +its optimizations come into play, and the problem handed to Kodkod is +essentially a first-order relational logic (FORL) rendering of the TPTP FOF +problem. There are two main exceptions: +<ul> +<li> Nested quantifiers are moved as far inside the formula as possible before +Kodkod 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 Isabelle +itself, which adheres to the LCF small-kernel discipline, Nitrox does not +certify its results and must be trusted. Kodkod is written in Java. MiniSat 1.14 +is 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 it +a bit (but not as much as the missing type inference). Kodkod itself is known to +perform less well on FOF than Paradox, because it is designed and optimized for +a somewhat different logic, FORL. On the other hand, Kodkod's symmetry breaking +might be better calibrated than Paradox's. Hence, we expect Nitrox to end up in +second 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><!------------------------------------------------------------------------>

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/CASC/SysDesc_Refute.html Tue May 21 11:01:14 2013 +0200 @@ -0,0 +1,55 @@ +<HR><!------------------------------------------------------------------------> +<H2>Refute 2013</H2> +Jasmin C. Blanchette<sup>1</sup>, Tjark Weber<sup>2</sup><BR> +<sup>1</sup>Technische Universität München, Germany <BR> +<sup>2</sup>Uppsala Universitet, Sweden <BR> + +<H3>Architecture</H3> + +Refute [<A HREF="#References">Web08</A>] is an open source counterexample +generator for Isabelle/HOL [<A HREF="#References">NPW13</A>] based on a +SAT solver, and Nitpick's [<A HREF="#References">BN10</A>] precursor. + +<H3>Strategies</H3> + +<p> +Refute employs a SAT solver to find a finite model of the negated conjecture. +The translation from HOL to propositional logic is parameterized by the +cardinalities of the atomic types occurring in the conjecture. Refute enumerates +the possible cardinalities for each atomic type. If a formula has a finite +counterexample, the tool eventually finds it, unless it runs out of resources. + +<H3>Implementation</H3> + +<p> +Refute, like most of Isabelle/HOL, is written in Standard ML. Unlike Isabelle +itself, which adheres to the LCF small-kernel discipline, Refute does not +certify its results and must be trusted. +<P> +Refute is available as part of Isabelle/HOL for all major platforms under a +BSD-style license from +<PRE> + <A HREF="http:////www.cl.cam.ac.uk/research/hvg/Isabelle/">http://www.cl.cam.ac.uk/research/hvg/Isabelle</A></PRE> + +<H3>Expected Competition Performance</H3> + +We expect that Refute will solve about 75% of the problems solved by Nitpick in +the TNT category, and perhaps a few problems that Nitpick cannot solve. + +<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> Web08 +<DD> Weber T. (2008), + <STRONG>SAT-based Finite Model Generation for Higher-Order Logic</STRONG>, Ph.D. thesis. +</DL> +<P> + +<HR><!------------------------------------------------------------------------>