[isabelle-dev] Z3_Proof_Reconstruction

[Johannes Gareis]

Sehr geehrtes Isabelle-Team,


ich beschäftige mich zur Zeit mit dem SMT-Solver Z3 und bin auf ein paar 
Paper ihrer Gruppe zum Thema Proof Reconstruction in Z3 gestoßen.

Nun habe ich Isabelle installiert und etwas damit rumgespielt, kann aber 
nicht herausfinden, wie ich einen UNSAT-Proof von Z3 an Isabelle geben 
kann, um diesen zu überprüfen. Leider finde ich in eurer 
Isabelle-Dokumentation auch nicht das passende dazu.


Könnten Sie mir sagen, wie ich Isabelle aufrufen/bedienen muss, um einen 
UNSAT-Proof zu testen?


Mit freundlichen Grüßen,

Johannes Gareis



-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5304 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160817/bd5a556a/attachment.p7s>