参考:
Proofs and refutations, and Z3
http://research.microsoft.com/en-us/um/people/leonardo/iwil08.pdf
https://twitter.com/masahiro_sakai/status/790940253364248576
使った例:
(set-option :produce-proofs true)
(set-option :produce-unsat-cores true)
(set-logic QF_LRA)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(assert (! (>= (+ x1 x2 x3) 1) :named c1))
(assert (! (>= (+ (- x1) x2) 0) :named c2))
(assert (! (>= (+ (- x2) x3) 0) :named c3))
(assert (! (>= (- x3) 0) :named c4))
(assert (! (>= (+ x2 (- x3)) 0) :named c5))
(assert (! (>= (+ (- x2) (- x3)) (- 1)) :named c6))
(assert (! (>= (+ (- x2) x3) 0) :named c7))
(check-sat)
;=> unsat
(get-unsat-core)
;=> (c1 c2 c3 c4)
(get-proof)
;=>
; ((set-logic QF_LRA)
; (declare-fun c3 () Bool)
; (declare-fun c1 () Bool)
; (declare-fun c2 () Bool)
; (declare-fun c4 () Bool)
; (proof
; (let ((?x100 (* (- 1.0) x3)))
; (let ((?x101 (+ x2 ?x100)))
; (let (($x102 (<= ?x101 0.0)))
; (let (($x105 (or (not c3) $x102)))
; (let ((@x107 (monotonicity (rewrite (= (>= (+ (* (- 1.0) x2) x3) 0.0) $x102)) (= (or (not c3) (>= (+ (* (- 1.0) x2) x3) 0.0)) $x105))))
; (let (($x88 (>= (+ (* (- 1.0) x2) x3) 0.0)))
; (let (($x95 (or (not c3) $x88)))
; (let (($x79 (>= (+ (- x2) x3) 0.0)))
; (let (($x81 (=> c3 $x79)))
; (let ((@x87 (monotonicity (rewrite (= (- x2) (* (- 1.0) x2))) (= (+ (- x2) x3) (+ (* (- 1.0) x2) x3)))))
; (let ((@x93 (monotonicity (monotonicity @x87 (= $x79 $x88)) (= $x81 (=> c3 $x88)))))
; (let ((@x109 (trans (trans @x93 (rewrite (= (=> c3 $x88) $x95)) (= $x81 $x95)) @x107 (= $x81 $x105))))
; (let ((@x110 (mp (asserted $x81) @x109 $x105)))
; (let (($x32 (>= (+ x1 x2 x3) 1.0)))
; (let (($x37 (or (not c1) $x32)))
; (let ((@x42 (mp (asserted (=> c1 $x32)) (rewrite (= (=> c1 $x32) $x37)) $x37)))
; (let (($x68 (<= (+ x1 (* (- 1.0) x2)) 0.0)))
; (let (($x71 (or (not c2) $x68)))
; (let ((@x73 (monotonicity (rewrite (= (>= (+ (* (- 1.0) x1) x2) 0.0) $x68)) (= (or (not c2) (>= (+ (* (- 1.0) x1) x2) 0.0)) $x71))))
; (let (($x54 (>= (+ (* (- 1.0) x1) x2) 0.0)))
; (let (($x61 (or (not c2) $x54)))
; (let (($x43 (>= (+ (- x1) x2) 0.0)))
; (let (($x45 (=> c2 $x43)))
; (let ((@x53 (monotonicity (rewrite (= (- x1) (* (- 1.0) x1))) (= (+ (- x1) x2) (+ (* (- 1.0) x1) x2)))))
; (let ((@x59 (monotonicity (monotonicity @x53 (= $x43 $x54)) (= $x45 (=> c2 $x54)))))
; (let ((@x75 (trans (trans @x59 (rewrite (= (=> c2 $x54) $x61)) (= $x45 $x61)) @x73 (= $x45 $x71))))
; (let ((@x76 (mp (asserted $x45) @x75 $x71)))
; (let (($x130 (<= x3 0.0)))
; (let (($x133 (or (not c4) $x130)))
; (let ((@x135 (monotonicity (rewrite (= (>= ?x100 0.0) $x130)) (= (or (not c4) (>= ?x100 0.0)) $x133))))
; (let (($x118 (>= ?x100 0.0)))
; (let (($x125 (or (not c4) $x118)))
; (let ((?x111 (- x3)))
; (let (($x112 (>= ?x111 0.0)))
; (let (($x114 (=> c4 $x112)))
; (let ((@x123 (monotonicity (monotonicity (rewrite (= ?x111 ?x100)) (= $x112 $x118)) (= $x114 (=> c4 $x118)))))
; (let ((@x137 (trans (trans @x123 (rewrite (= (=> c4 $x118) $x125)) (= $x114 $x125)) @x135 (= $x114 $x133))))
; (let ((@x138 (mp (asserted $x114) @x137 $x133)))
; ((_ th-lemma arith farkas 3/2 1/2 1/2 1) (unit-resolution @x138 (asserted c4) $x130) (unit-resolution @x76 (asserted c2) $x68) (unit-resolution @x42 (asserted c1) $x32) (unit-resolution @x110 (asserted c3) $x102) false)))))))))))))))))))))))))))))))))))))))))
