[isabelle-dev] Z3_Proof_Reconstruction

[boehmes at in.tum.de]

Hi Johannes,

Note that emails are typically written in English on this mailing list.

Isabelle uses Z3 to find proofs for goals that are formulated by users. The query to Z3 is generated by Isabelle. The UNSAT answer from Z3, i.e., the proof trace, is parsed by Isabelle, which then tries to replay the proof to yield an Isabelle theorem.

Your application is somewhat different. It seems that you only want to use the replay functionality of Isabelle. This is not that easy with the structure of the existing code. Look at src/HOL/Tools/SMT/z3_replay.ML as an entry point to the replay code. I suggest, however, to formulate your problem as an Isabelle proof obligation, e.g. a lemma, and apply the “smt” method:

lemma fixes P :: bool assumes P shows P
  using assms [[smt_trace]] by smt

The output of the smt method shows the entire interaction with Z3.

Cheers,
Sascha

Von: Johannes Gareis
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160819/95fc97ca/attachment.html>