Montag, 19. November 2012

Verifiying proofs with Z3

The Z3 theorem prover has a command for constructing proofs: (get-proof). The resulting files are not meant "for human consumption" and you can probably see why:

unsat
((set-logic <null>)
(proof
(let ((@x41 (monotonicity (rewrite (= (<= 2 a) (>= a 2))) (= (not (<= 2 a)) (not (>= a 2))))))
(let (($x19 (<= 2 a)))
(let (($x20 (not $x19)))
(let ((@x26 (monotonicity (rewrite (= $x19 $x19)) (= $x20 $x20))))
(let ((@x27 (trans (rewrite (= (< a 2) $x20)) @x26 (= (< a 2) $x20))))
(let (($x7 (< a 2)))
(let ((@x29 (mp (mp (|and-elim| (asserted (and (> a 3) $x7)) $x7) @x27 $x20) @x26 $x20)))
(let ((@x42 (mp (mp (mp @x29 (|rewrite*| (= $x20 $x20)) $x20) @x26 $x20) @x41 (not (>= a 2)))))
(let (($x39 (>= a 2)))
(let (($x15 (not (<= a 3))))
(let ((@x18 (mp (|and-elim| (asserted (and (> a 3) $x7)) (> a 3)) (rewrite (= (> a 3) $x15)) $x15)))
(let ((@x64 (|unit-resolution| ((_ |th-lemma| arith farkas 1 1) (or $x39 (<= a 3))) (mp @x18 (|rewrite*| (= $x15 $x15)) $x15) $x39)))
(|unit-resolution| @x64 @x42 false)))))))))))))))
Looking good, right? Well, hardly.
Even with nicer formatting, line breaks, etc. the proof is not quite readable. Now, it looks like people have actually managed to work with these proofs and I'm quite curious about how they accomplished that. There is a description of all the symbols used in the proof, but what I'm lacking is some kind of command line parameter which simply feeds the proof back into Z3.

If I ever find one (or build one), I'll write down here.

Keine Kommentare:

Kommentar veröffentlichen