1(* Title: HOL/SAT.thy 2 Author: Alwen Tiu, Tjark Weber 3 Copyright 2005 4 5Basic setup for the 'sat' and 'satx' tactics. 6*) 7 8section \<open>Reconstructing external resolution proofs for propositional logic\<close> 9 10theory SAT 11imports Argo 12begin 13 14ML_file \<open>Tools/prop_logic.ML\<close> 15ML_file \<open>Tools/sat_solver.ML\<close> 16ML_file \<open>Tools/sat.ML\<close> 17ML_file \<open>Tools/Argo/argo_sat_solver.ML\<close> 18 19method_setup sat = \<open>Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac)\<close> 20 "SAT solver" 21 22method_setup satx = \<open>Scan.succeed (SIMPLE_METHOD' o SAT.satx_tac)\<close> 23 "SAT solver (with definitional CNF)" 24 25end 26