14350

1 
(* Title: HOL/Refute.thy


2 
ID: $Id$


3 
Author: Tjark Weber


4 
Copyright 20032004


5 


6 
Basic setup and documentation for the 'refute' (and 'refute_params') command.


7 
*)


8 

14589

9 
header {* Refute *}


10 


11 
theory Refute = Map


12 


13 
files "Tools/prop_logic.ML"


14 
"Tools/sat_solver.ML"


15 
"Tools/refute.ML"


16 
"Tools/refute_isar.ML":


17 


18 
setup Refute.setup


19 


20 
text {*


21 
\small


22 
\begin{verbatim}

14350

23 
(*  *)


24 
(* REFUTE *)


25 
(* *)


26 
(* We use a SAT solver to search for a (finite) model that refutes a given *)


27 
(* HOL formula. *)


28 
(*  *)


29 


30 
(*  *)

14457

31 
(* NOTE *)

14350

32 
(* *)

14457

33 
(* I strongly recommend that you install a standalone SAT solver if you *)

14463

34 
(* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. If you *)

14808

35 
(* have installed ZChaff Version 2003.12.04, simply set 'ZCHAFF_HOME' in *)


36 
(* 'etc/settings'. *)

14350

37 
(*  *)


38 


39 
(*  *)


40 
(* USAGE *)


41 
(* *)


42 
(* See the file 'HOL/ex/Refute_Examples.thy' for examples. The supported *)


43 
(* parameters are explained below. *)


44 
(*  *)


45 


46 
(*  *)


47 
(* CURRENT LIMITATIONS *)


48 
(* *)


49 
(* 'refute' currently accepts formulas of higherorder predicate logic (with *)


50 
(* equality), including free/bound/schematic variables, lambda abstractions, *)

14808

51 
(* sets and set membership, "arbitrary", "The", and "Eps". Defining *)


52 
(* equations for constants are added automatically. Inductive datatypes are *)


53 
(* supported, but may lead to spurious countermodels. *)

14463

54 
(* *)

14808

55 
(* The (space) complexity of the algorithm is nonelementary. *)

14350

56 
(* *)


57 
(* NOT (YET) SUPPORTED ARE *)


58 
(* *)


59 
(*  schematic type variables *)

14463

60 
(*  axioms, sorts *)


61 
(*  inductively defined sets *)

14808

62 
(*  recursive functions on IDTs (case, recursion operators, size) *)

14463

63 
(*  ... *)

14350

64 
(*  *)


65 


66 
(*  *)


67 
(* PARAMETERS *)


68 
(* *)


69 
(* The following global parameters are currently supported (and required): *)


70 
(* *)


71 
(* Name Type Description *)


72 
(* *)


73 
(* "minsize" int Only search for models with size at least *)


74 
(* 'minsize'. *)


75 
(* "maxsize" int If >0, only search for models with size at most *)


76 
(* 'maxsize'. *)


77 
(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)


78 
(* when transforming the term into a propositional *)


79 
(* formula. *)

14808

80 
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *)


81 
(* This value is ignored under some ML compilers. *)

14457

82 
(* "satsolver" string Name of the SAT solver to be used. *)


83 
(* *)


84 
(* See 'HOL/Main.thy' for default values. *)

14808

85 
(* *)


86 
(* The size of particular types can be specified in the form type=size *)


87 
(* (where 'type' is a string, and 'size' is an int). Examples: *)


88 
(* "'a"=1 *)


89 
(* "List.list"=2 *)

14350

90 
(*  *)


91 


92 
(*  *)


93 
(* FILES *)


94 
(* *)

14457

95 
(* HOL/Tools/prop_logic.ML Propositional logic *)


96 
(* HOL/Tools/sat_solver.ML SAT solvers *)


97 
(* HOL/Tools/refute.ML Translation HOL > propositional logic and *)

14808

98 
(* Boolean assignment > HOL model *)

14350

99 
(* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *)

14457

100 
(* syntax *)


101 
(* HOL/Refute.thy This file: loads the ML files, basic setup, *)


102 
(* documentation *)


103 
(* HOL/Main.thy Sets default parameters *)


104 
(* HOL/ex/RefuteExamples.thy Examples *)

14350

105 
(*  *)

14589

106 
\end{verbatim}


107 
*}

14350

108 


109 
end
