z3 是否支持证明归纳事实？答案

【问题标题】：does z3 support proving inductive facts at all?z3 是否支持证明归纳事实？
【发布时间】：2017-08-29 19:46:03
【问题描述】：

我了解 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)

现在它只是在我的机器上永远循环。

【问题讨论】：

标签： z3

【解决方案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

【讨论】：