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



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to