[isabelle-dev] smt in the repository

[Tobias Nipkow]

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.

Tobias

On 26/05/2020 17:12, Manuel Eberl wrote:
> If I recall correctly, Z3 is open source and bundled with Isabelle, so
> there is no problem in that regard.
> 
> The only problem I can think of is that these proofs are unreadable and
> tend to break frequently. But the same is true for "metis" proofs. I
> avoid both of them wherever I can for that reason, but it would be
> unrealistic to set this as a general policy.
> 
> So unless there is some problem with it that I am unaware of, I think
> our policy should be "accepted, but perhaps frowned upon just a little
> bit by some people". :)
> 
> Manuel
> 
> 
> On 26/05/2020 17:09, Lawrence Paulson wrote:
>> What is our policy on use of the smt method at the moment? Prohibited, frowned upon, okay? Getting rid of it can take a lot of work.
>>
>> Larry
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- 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/ae1f5275/attachment.bin>