Re: [isabelle] Finite Datatype


On Fri, 2008-06-06 at 17:08 +0200, Tobias Nipkow wrote:
> Since this is in essence a finite problem, Tjark Weber's SAT-solver link 
> may be able to prove this automatically. Tjark?

I am afraid the SAT solver link currently works for (instances of)
propositional tautologies only.  (However, link-ups with other automated
provers for more powerful logics are available as well.  See, e.g.,
metis and sledgehammer.)  I suspect that in your case the performance
issue shows up before the proof goal is purely propositional.

If you want to send me your proof though, I'll be happy to look at it in
more detail.


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