Re: [isabelle] Uses of 'sat' method
On Friday 04 November 2005 21:14, Oliver Pell wrote:
> What kind of goals can be solved using the 'sat' method in Isabelle2005?
> I have installed zChaff and have the SAT_Examples.thy file working, but
> I was wondering whether its actually possible to use sat as a practical
> decision method in proofs.
the 'sat' method has been improved significantly since the Isabelle2005
release; therefore I strongly recommend that you use the Isabelle development
version  instead. In Isabelle2005, 'sat' requires your subgoal to be of
the form "Premises ==> False", as shown in HOL/ex/SAT_Examples.thy. This is
no longer the case in the development version.
Please note that 'sat' in any case only considers the propositional structure
of a formula, e.g. quantified subformulas are treated as atomic. Hence only
(instances of) *propositional* tautologies can be proved by 'sat'.
I am afraid there is little documentation available aside from
HOL/ex/SAT_Examples.thy, but you can find the implementation of 'sat' in
HOL/Tools/cnf_funcs.ML and HOL/Tools/sat_funcs.ML. Suggestions for
improvement are welcome.
This archive was generated by a fusion of
Pipermail (Mailman edition) and