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