Có hỗ trợ Z3 Craig Interpolation

Question

Z3 có thể tạo ra các nội suy Craig (ít nhất là cho logic mệnh đề không?). Tôi chưa tìm thấy nó trong tài liệu của Z3.

Answer 1

Không, Z3 không hỗ trợ nội suy Craig, nhưng nó tạo ra bằng chứng. Các nội suy có thể được trích xuất từ ​​các bằng chứng. Ken Mcmillan đang phát triển một máy phát nội suy trên đỉnh Z3 bằng cách sử dụng phương pháp này.