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 [1] 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.

Best regards,


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.