[isabelle-dev] smt in the repository

[Tobias Nipkow]

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.
> 
> Larry
> 
>> On 26 May 2020, at 16:58, Tobias Nipkow <nipkow at in.tum.de> 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.
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200526/7eff1348/attachment.bin>