[isabelle-dev] smt in the repository
eberlm at in.tum.de
Tue May 26 17:12:44 CEST 2020
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
More information about the isabelle-dev