[isabelle-dev] smt in the repository
nipkow at in.tum.de
Tue May 26 17:58:10 CEST 2020
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.
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". :)
> 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.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev