[isabelle] Uses of 'sat' method



Hi,

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.

For example, I have a HOL proof which decomposes into many sub-goals which are simple first order propositional logic formulae. I've been using a combination of case-splitting and 'auto' to solve these, but is it possible to use the sat method instead?

One example of such a goal (though simpler than most) is:
!!a b c d. [| x = (True, a, p1); y = (True, b, p2); z = (True, c, p3) |] ==> (c --> d = b --> (EX a. a)) & (~ c --> d = a --> (EX a. a))

"apply sat" reports a countermodel of the premises. Similarly, the theorem "[| x ; y |] ==> x --> y" can't be solved by sat (countermodel {y, x}) but can be solved by "rule impI" then "by sat".

Is there any way to automatically pre-process goals into a suitable form for the SAT solver? Or is there any other documentation for this?

Thanks,

Oliver.





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