diff -r f353fe3c2b92 -r 6c38df1d294a src/HOL/TPTP/CASC/SysDesc_Refute.html --- /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 @@ +

Refute 2013

+Jasmin C. Blanchette¹, Tjark Weber²
+¹Technische Universität München, Germany
+²Uppsala Universitet, Sweden
+ +

Architecture

+ +Refute [Web08] is an open source counterexample +generator for Isabelle/HOL [NPW13] based on a +SAT solver, and Nitpick's [BN10] precursor. + +

Strategies

+ +

+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. + +

Implementation

+ +

+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. +

+Refute 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

+ +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. + +

References

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. +
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. +
Web08 +: Weber T. (2008), + SAT-based Finite Model Generation for Higher-Order Logic, Ph.D. thesis. +

+ +