C-D22-IMPLICIT-STATE

Kiến trúc CEGAR implicit D22 CHỨNG-MINH-VỮNG: giữ đối tượng toàn cục có chặn dạng symbolic (coefficient master E_j và root master X_i), chiếu xuống từng prime, hỏi bài con thu hẹp (MATCH-WITNESS / EMPTY-CERTIFIED / OPEN-INCOMPLETE) và sinh cut mang chứng minh là vững theo định lý một-chiều: một phản ví dụ có chặn sống sót mọi cut chứng nhận (phủ nền của nó khớp tại mọi prime, nên một cut empty-certified không thể chứa nó; các cut applicability và square-splitting cũng loại nó). Không cut chứng nhận nào loại một phản ví dụ

Nói dễ hiểu

Kiến trúc symbolic-và-cut được chứng minh an toàn: không cut mang chứng minh nào có thể vứt bỏ một phản ví dụ thật.

Phát biểu chính xác

Kiến trúc CEGAR implicit D22 CHỨNG-MINH-VỮNG: giữ đối tượng toàn cục có chặn dạng symbolic (coefficient master E_j và root master X_i), chiếu xuống từng prime, hỏi bài con thu hẹp (MATCH-WITNESS / EMPTY-CERTIFIED / OPEN-INCOMPLETE) và sinh cut mang chứng minh là vững theo định lý một-chiều: một phản ví dụ có chặn sống sót mọi cut chứng nhận (phủ nền của nó khớp tại mọi prime, nên một cut empty-certified không thể chứa nó; các cut applicability và square-splitting cũng loại nó). Không cut chứng nhận nào loại một phản ví dụ