|
1 <HR><!------------------------------------------------------------------------> |
|
2 <H2>Refute 2013</H2> |
|
3 Jasmin C. Blanchette<sup>1</sup>, Tjark Weber<sup>2</sup><BR> |
|
4 <sup>1</sup>Technische Universität München, Germany <BR> |
|
5 <sup>2</sup>Uppsala Universitet, Sweden <BR> |
|
6 |
|
7 <H3>Architecture</H3> |
|
8 |
|
9 Refute [<A HREF="#References">Web08</A>] is an open source counterexample |
|
10 generator for Isabelle/HOL [<A HREF="#References">NPW13</A>] based on a |
|
11 SAT solver, and Nitpick's [<A HREF="#References">BN10</A>] precursor. |
|
12 |
|
13 <H3>Strategies</H3> |
|
14 |
|
15 <p> |
|
16 Refute employs a SAT solver to find a finite model of the negated conjecture. |
|
17 The translation from HOL to propositional logic is parameterized by the |
|
18 cardinalities of the atomic types occurring in the conjecture. Refute enumerates |
|
19 the possible cardinalities for each atomic type. If a formula has a finite |
|
20 counterexample, the tool eventually finds it, unless it runs out of resources. |
|
21 |
|
22 <H3>Implementation</H3> |
|
23 |
|
24 <p> |
|
25 Refute, like most of Isabelle/HOL, is written in Standard ML. Unlike Isabelle |
|
26 itself, which adheres to the LCF small-kernel discipline, Refute does not |
|
27 certify its results and must be trusted. |
|
28 <P> |
|
29 Refute is available as part of Isabelle/HOL for all major platforms under a |
|
30 BSD-style license from |
|
31 <PRE> |
|
32 <A HREF="http:////www.cl.cam.ac.uk/research/hvg/Isabelle/">http://www.cl.cam.ac.uk/research/hvg/Isabelle</A></PRE> |
|
33 |
|
34 <H3>Expected Competition Performance</H3> |
|
35 |
|
36 We expect that Refute will solve about 75% of the problems solved by Nitpick in |
|
37 the TNT category, and perhaps a few problems that Nitpick cannot solve. |
|
38 |
|
39 <H3>References</H3> |
|
40 <DL> |
|
41 <DT> BN10 |
|
42 <DD> Blanchette J. C., Nipkow T. (2010), |
|
43 <STRONG>Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder</STRONG>, |
|
44 ITP 2010, <EM>LNCS</EM> 6172, pp. 131–146, Springer. |
|
45 <DT> NPW13 |
|
46 <DD> Nipkow T., Paulson L. C., Wenzel M. (2013), |
|
47 <STRONG>Isabelle/HOL: A Proof Assistant for Higher-Order Logic</STRONG>, |
|
48 <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>. |
|
49 <DT> Web08 |
|
50 <DD> Weber T. (2008), |
|
51 <STRONG>SAT-based Finite Model Generation for Higher-Order Logic</STRONG>, Ph.D. thesis. |
|
52 </DL> |
|
53 <P> |
|
54 |
|
55 <HR><!------------------------------------------------------------------------> |