On Thu, 2013-08-01 at 16:41 +0200, Makarius wrote: > On Wed, 10 Jul 2013, Tjark Weber wrote: > Looking superficially at > http://isabelle.in.tum.de/repos/isabelle/file/b7a83845bc93/src/HOL/ex/SAT_Examples.thy > > I wonder if this actually works right now.
Good question. One issue is that the theory requires a SAT solver (zChaff or MiniSat) to work properly. These days, one could probably be shipped as a component, but I wonder if that's worth it. People just don't seem to use Isabelle to prove large propositional tautologies. I still think that encodings of decidable problems into propositional logic could probably be just as beneficial in theorem proving as they've been in many other domains. But regarding the future of "sat", I am rather undecided at this point. Best, Tjark _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
