Re: [isabelle] changing smt by automatic reasoning internal to Isabelle



Hi,

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?

Best wishes,
Dominique.



On 7/31/19 12:01 AM, lammich at in.tum.de wrote:
Hi Jose

Smt can be used, as it replays the proof in the kernel, only smt_oracle is ruled out.

Best
Peter


-------- Original Message --------
Subject: [isabelle] changing smt by automatic reasoning internal to Isabelle
From: José Manuel Rodríguez Caballero <josephcmac at gmail.com>
To: isabelle-users at cl.cam.ac.uk
CC:


    Dear Isabelle users and experts,
    In the rules for submissions to Archives of Formal Proofs, it is
    written
    that "No use of the command smt_oracle". If I well understood,
    this means
    that proofs cannot be done using either "apply smt" or "by smt"
    (please
    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
    over longer
    time"): http://proofcraft.org/blog/isabelle-style.html

    (i) Is there an automatic way to change "smt" by some automatic
    reasoning
    internal to Isabelle, e.g., metis, auto, simp?

    (ii) In case of a negative answer for (i), which are the steps "by
    hand"
    recommended for such a task?

    Sincerely yours,
    José M.

    --

    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 MHonArc.