Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Still no smt commands allowed in AFP submissions?

Email Gateway (Aug 19 2022 at 16:08):

From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle experts,

When I am checking the AFP submission guidelines, it requires no smt
command in proofs. I thought proof reconstructions for smt solvers
should be quite mature now. Shall I still need to eliminate all smt
commands from my proofs before submission to AFP?

Many thanks,
Wenda

Email Gateway (Aug 19 2022 at 16:08):

From: Tobias Nipkow <nipkow@in.tum.de>
On 13/09/2014 23:00, Wenda Li wrote:

Dear Isabelle experts,

When I am checking the AFP submission guidelines, it requires no smt command in
proofs. I thought proof reconstructions for smt solvers should be quite mature
now. Shall I still need to eliminate all smt commands from my proofs before
submission to AFP?

I am afraid so. There are maintenance issues otherwise.

Tobias

Many thanks,
Wenda

Last updated: Apr 25 2024 at 16:19 UTC