val SAT_TAUT_PROVE : Term.term -> Thm.thm
STRUCTURE
HolSatLib
SYNOPSIS
Proves that the supplied term is a tautology.
DESCRIBE
The supplied term should be a term of propositional logic. SAT_TAUT_PROVE uses the MiniSat SAT solver’s proof logging feature to construct a resolution refutation for the negation of the supplied term.
FAILURE
Fails if the supplied term is not a tautology. In this case, a theorem providing a satisfying assignment for the negation of the input term is returned, wrapped in an exception.
EXAMPLE
- load "HolSatLib"; open HolSatLib;
(* output omitted *)
> val it = () : unit
- SAT_TAUT_PROVE ``(a ==> b) /\ (b ==> a) ==> (a=b)``;
> val it = |- (a ==> b) /\ 2(b ==> a) ==> (a = b) : thm
- SAT_TAUT_PROVE ``~((a ==> b) /\ (b ==> a) ==> (a=b))`` 
	handle minisatProve.Sat_counterexample th => th;
> val it = |- ~b /\ a ==> ~~((a ==> b) /\ (b ==> a) ==> (a = b)) : thm
COMMENTS
If MiniSat terminates abnormally, or if the MiniSat binary cannot be located or executed, SAT_TAUT_PROVE falls back to a slower propositional tautology prover implemented in ML.
SEEALSO
satOracle, satProve
HOL  Kananaskis-4