Z3 と拡張 SMT-LIB2 構文を使用してホーン句を解決しています。角節の先頭は解釈されない述語であるべきだということはわかっています。しかし、次の節をどのようにホーン節の集合に書き直せばよいのだろうか。
(declare-rel inv (Int Int ))
(declare-var k Int)
(declare-var k_p Int)
(declare-var a Int)
(declare-var a_p Int)
(rule (=> (and (= a 0) (= k 0)) (inv a k)))
(rule (=> (and (inv a k) (= a_p (+ a 1))(= k_p (+ k 1))) (inv a_p k_p)))
(rule (=> (and (inv a k) (> k 0) ) (> a 0)))
(query inv )
Z3(> a 0)は、ホーン節の先頭になれないと不平を言っています。最後の節を次のように書き直すことができます。
(rule (=> (and (inv a k) (> k 0) ) (gtz a)))
(rule (=> (> a 0) (gtz a)))
しかし、その後、句が非常に弱くなり、 invariant の意図したモデルが得られなくなりますinv。これを行うためのより良い方法があるかどうか疑問に思います。