Re: [isabelle] changing smt by automatic reasoning internal to Isabelle
I noticed that until October 2017, the submission instructions for AFP
also contained "No use of the command <code>smt</code>. The result of
this command depends on external tools that are not under our control
and may stop working in the future."
This was removed in commit 48c7802 (afp-devel) by Gerwin Klein.
I am curious why this is no longer a necessity? As I understood, the
reason was not the fact that the proof is not replayed (as in the case
of smt_oracle), but that the behavior of smt depends on Z3, and thus
breaks easily when Z3 changes.
Is my understanding correct? Has this situation changed? Or has merely
the policy changed and the expectation is that smt proofs are just fixed
once Z3 changes make them the smt proofs break?
On 7/31/19 12:01 AM, lammich at in.tum.de wrote:
Smt can be used, as it replays the proof in the kernel, only
smt_oracle is ruled out.
-------- Original Message --------
Subject: [isabelle] changing smt by automatic reasoning internal to
From: José Manuel Rodríguez Caballero <josephcmac at gmail.com>
To: isabelle-users at cl.cam.ac.uk
Dear Isabelle users and experts,
In the rules for submissions to Archives of Formal Proofs, it is
that "No use of the command smt_oracle". If I well understood,
that proofs cannot be done using either "apply smt" or "by smt"
correct me if I am wrong). This was also pointed out in Gerwin's Style
Guide (section: "Do not use smt in proofs you need to maintain
(i) Is there an automatic way to change "smt" by some automatic
internal to Isabelle, e.g., metis, auto, simp?
(ii) In case of a negative answer for (i), which are the steps "by
recommended for such a task?
José Manuel Rodríguez Caballero
arvutiteaduse instituut / Institute of Computer Science
Tartu Ülikool / University of Tartu
Personal Research Page: https://josephcmac.github.io/
This archive was generated by a fusion of
Pipermail (Mailman edition) and