Invokes supplied SAT solver on the argument term, returning a theorem if a model is found, otherwise throwing an exception.
DESCRIBE
The supplied term should be a term of propositional logic and must be in conjunctive normal form. satProve uses HOL to check the SAT solver’s model by evaluating the term for the values supplied by the model.
FAILURE
Fails if a model cannot be found for the supplied term, or if the SAT solver fails abnormally.
EXAMPLE
- load "HolSatLib"; open HolSatLib;
(* output omitted *)
> val it = () : unit
- satProve grasp ``(x \/ ~y \/ z) /\ (~z \/ y)``;
> val it = |- z /\ y ==> (x \/ ~y \/ z) /\ (~z \/ y) : thm
COMMENTS
If one is prepared to trust the solver, then one can use satOracle which returns a tagged theorem. The SAT solver must be a supported one: see the HolSat section of the HOL System Description for details.