[isabelle-dev] smt in the repository

[Manuel Eberl]

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
>