z3是否支持證明歸納事實？

Question

我知道z3無法驗證一般的歸納證明。不過我很好奇，如果有一種方法來使它檢查喜歡的東西很簡單：現在它只是循環永遠在我的機器上

; returns the same input list after iterating through each element 
(declare-fun iterate ((List Int)) (List Int)) 

(declare-const l (List Int)) 

(assert (forall ((l (List Int))) 
    (ite (= l nil) 
    (= (iterate l) nil) 
    (= (iterate l) (insert (head l) (iterate (tail l)))) 
) 
)) 

(assert (not (= l (iterate l)))) 
(check-sat) 

。

Answer 1

Z3不會自行進行歸納論證。你可以手動給它一個歸納假設，並要求它完成證明。這適用於您的示例如下：

(declare-fun iterate ((List Int)) (List Int)) 

(assert (forall ((l (List Int))) 
    (ite (= l nil) 
    (= (iterate l) nil) 
    (= (iterate l) (insert (head l) (iterate (tail l))))))) 

; define list length for convenience in stating the induction hypothesis 
(declare-fun length ((List Int)) Int) 
(assert (= (length nil) 0)) 
(assert (forall ((x Int) (l (List Int))) 
    (= (length (insert x l)) (+ 1 (length l))))) 

(declare-const l (List Int)) 

; here comes the induction hypothesis: 
; that the statement is true for all lists shorter than l 
(assert (forall ((ihl (List Int))) 
    (=> (< (length ihl) (length l)) 
     (= ihl (iterate ihl))))) 

; we now ask Z3 to show that the result follows for l   
(assert (not (= l (iterate l)))) 
(check-sat) ; reports unsat as desired