Christian Zimmerer (Nov 13 2022 at 12:42): Christian Zimmerer (Nov 13 2022 at 12:42):Hi, I am trying to pull a complement into a union of sets, but somehow Isabelle doesn't see that you can do that.
I'm currently stuck here and would appreciate some help :D
Christian Zimmerer (Nov 13 2022 at 12:46):Nvm, that statement is false. I should have turned the union into an intersect
Notification Bot (Nov 13 2022 at 12:46):Christian Zimmerer has marked this topic as resolved.
Manuel Eberl (Nov 14 2022 at 10:44):Just a general remark: auto and especially blast are very good with first-order logic, so if they claim something does not hold it probably doesn't. "blast" should even be complete for first-order logic. There are instances where something is a valid statement in first-order logic but "blast" seemingly never terminates, but I don't recall ever seeing it terminate without proving a true FOL statement.
Last updated: Apr 20 2024 at 04:19 UTC