<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=utf-8"><meta name=Generator content="Microsoft Word 15 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:70.85pt 70.85pt 2.0cm 70.85pt;}
div.WordSection1
{page:WordSection1;}
--></style></head><body lang=DE link=blue vlink="#954F72"><div class=WordSection1><p class=MsoNormal>Hi Johannes,<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><span lang=EN-US>Note that emails are typically written in English on this mailing list.<o:p></o:p></span></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><span lang=EN-US>Isabelle uses Z3 to find proofs for goals that are formulated by users. The query to Z3 is </span><span lang=EN-GB>generated by </span><span lang=EN-US>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.<o:p></o:p></span></p><p class=MsoNormal><span lang=EN-US><o:p> </o:p></span></p><p class=MsoNormal><span lang=EN-US>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:<o:p></o:p></span></p><p class=MsoNormal><span lang=EN-US><o:p> </o:p></span></p><p class=MsoNormal><span lang=EN-US>lemma fixes P :: bool assumes P shows P<o:p></o:p></span></p><p class=MsoNormal><span lang=EN-US> using assms [[smt_trace]] by smt<o:p></o:p></span></p><p class=MsoNormal><span lang=EN-US><o:p> </o:p></span></p><p class=MsoNormal><span lang=EN-US>The output of the smt method shows the entire interaction with Z3.<o:p></o:p></span></p><p class=MsoNormal><span lang=EN-US><o:p> </o:p></span></p><p class=MsoNormal><span lang=EN-US>Cheers,<o:p></o:p></span></p><p class=MsoNormal><span lang=EN-US>Sascha<o:p></o:p></span></p><p class=MsoNormal><span style='font-size:12.0pt;font-family:"Times New Roman",serif'><o:p> </o:p></span></p><div style='mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm'><p class=MsoNormal style='border:none;padding:0cm'><b>Von: </b><a href="mailto:johannes.gareis@uni-bamberg.de">Johannes Gareis</a><br><b>Gesendet: </b>Mittwoch, 17. August 2016 09:44<br><b>An: </b><a href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a><br><b>Betreff: </b>[isabelle-dev] Z3_Proof_Reconstruction</p></div><p class=MsoNormal><span style='font-size:12.0pt;font-family:"Times New Roman",serif'><o:p> </o:p></span></p><p class=MsoNormal>Sehr geehrtes Isabelle-Team,</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>ich beschäftige mich zur Zeit mit dem SMT-Solver Z3 und bin auf ein paar </p><p class=MsoNormal>Paper ihrer Gruppe zum Thema Proof Reconstruction in Z3 gestoßen.</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Nun habe ich Isabelle installiert und etwas damit rumgespielt, kann aber </p><p class=MsoNormal>nicht herausfinden, wie ich einen UNSAT-Proof von Z3 an Isabelle geben </p><p class=MsoNormal>kann, um diesen zu überprüfen. Leider finde ich in eurer </p><p class=MsoNormal>Isabelle-Dokumentation auch nicht das passende dazu.</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Könnten Sie mir sagen, wie ich Isabelle aufrufen/bedienen muss, um einen </p><p class=MsoNormal>UNSAT-Proof zu testen?</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Mit freundlichen Grüßen,</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Johannes Gareis</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p></div></body></html>