Email Gateway (Aug 17 2022 at 13:28): Email Gateway (Aug 17 2022 at 13:28):From: Tjark Weber <tjark.weber@gmx.de>
Oliver,
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,
Tjark
[1] http://isabelle.in.tum.de/devel/
Last updated: May 03 2024 at 08:18 UTC