On 26/05/2020 18:08, Lawrence Paulson wrote:
For a solver that is designed to cope with thousands of clauses, I would be surprised if it suffered such a regression that it could fail for the trivial problems we present to it. I’m not aware of an occasion when any of the 2400+ occurrences have ever failed.
Note that we don't just want any proof, we want proofs with proof objects that check, and we are the only consumers of those proof objects, and the Z3 designers always felt those proof objects are a pain.
The past is not always a good predictor of the future ;-) Tobias
I would also question the claim that they are unusually unreadable. The attached list of theorems tends to omit a lot of routine reasoning and therefore lists the critical three or four facts required for the proof. LarryOn 26 May 2020, at 16:58, Tobias Nipkow <[email protected]> wrote: Z3 ist not under our control. If it changes, those proofs may no longer work. Hence I am very sceptical of having them in the distribution.
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
