## Refute 2013

Jasmin C. Blanchette1, Tjark Weber2
1Technische Universität München, Germany
2Uppsala 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.