Khi một công thức trong Z3 không xác định và (có được bằng chứng) được xác định có một đầu ra mà tôi không tìm thấy bất kỳ thông tin nào về nó là gì. Tôi có thể tìm thấy bất kỳ tài liệu nào về điều đó?Đầu ra ví dụ của Z3
Dường như với tôi khá khó đọc, có thể có bất kỳ công cụ nào lấy điều này làm đầu vào không?
Chúc mừng, Matt
Các "chứng minh" được sản xuất bởi Z3 không cho con người. Phiên bản lỗi thời của định dạng được mô tả trong bài báo: Proofs and Refutations, and Z3. Tệp z3_api.h có mô tả dài về từng quy tắc chứng minh. Số nhận dạng quy tắc chứng minh bắt đầu bằng Z3_OP_PR. Tôi biết hai ứng dụng sử dụng các đối tượng bằng chứng Z3. Các giấy tờ sau đây chứa rất nhiều ví dụ và mô tả cách các đối tượng bằng chứng có thể được sử dụng.
1- Isabelle Định lý tương tác Prover: Chứng minh Z3 được xây dựng lại bên trong Isabelle sử dụng lõi tin cậy. Bạn có thể tìm thấy một số giấy tờ mô tả công việc này và định dạng bằng chứng Z3 tại Sascha Bohme's homepage
Như pad cho biết, unsat-cores là đơn giản hơn nhiều để sử dụng.
Cảm ơn rất nhiều về các liên kết của bạn. Tôi sẽ xem xét cả hai phương pháp. Vì vậy, cũng nhờ @pad! – MattKay
Lệnh '(get-unsat-core)' có vẻ là thứ bạn muốn. Ví dụ chính thức: http://rise4fun.com/Z3/smtc_core – pad