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 
use "Tools/prop_logic.ML"


19 
use "Tools/sat_solver.ML"


20 
use "Tools/refute.ML"


21 
use "Tools/refute_isar.ML"


22 


23 
setup Refute.setup


24 


25 
text {*


26 
\small


27 
\begin{verbatim}

14350

28 
(*  *)


29 
(* REFUTE *)


30 
(* *)


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


32 
(* HOL formula. *)


33 
(*  *)


34 


35 
(*  *)

14457

36 
(* NOTE *)

14350

37 
(* *)

14457

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

14463

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


40 
(* have installed ZChaff, simply set 'ZCHAFF_HOME' in 'etc/settings'. *)

14350

41 
(*  *)


42 


43 
(*  *)


44 
(* USAGE *)


45 
(* *)


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


47 
(* parameters are explained below. *)


48 
(*  *)


49 


50 
(*  *)


51 
(* CURRENT LIMITATIONS *)


52 
(* *)


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


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

14457

55 
(* sets and set membership, "arbitrary", "The", and "Eps". Constants for *)

14463

56 
(* which a defining equation exists are unfolded automatically. Non *)


57 
(* recursive inductive datatypes are supported. *)


58 
(* *)


59 
(* The (space) complexity of the algorithm is exponential in both the length *)


60 
(* of the formula and the size of the model. *)

14350

61 
(* *)


62 
(* NOT (YET) SUPPORTED ARE *)


63 
(* *)


64 
(*  schematic type variables *)

14463

65 
(*  axioms, sorts *)


66 
(*  type constructors other than bool, =>, set, nonrecursive IDTs *)


67 
(*  inductively defined sets *)


68 
(*  recursive functions *)


69 
(*  ... *)

14350

70 
(*  *)


71 


72 
(*  *)


73 
(* PARAMETERS *)


74 
(* *)


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


76 
(* *)


77 
(* Name Type Description *)


78 
(* *)


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


80 
(* 'minsize'. *)


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


82 
(* 'maxsize'. *)


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


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


85 
(* formula. *)

14457

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


87 
(* *)


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

14350

89 
(*  *)


90 


91 
(*  *)


92 
(* FILES *)


93 
(* *)

14457

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


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


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


97 
(* boolean assignment > HOL model *)

14350

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

14457

99 
(* syntax *)


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


101 
(* documentation *)


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


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

14350

104 
(*  *)

14589

105 
\end{verbatim}


106 
*}

14350

107 


108 
end
