这些条款的等效horn条款是什么？

Question

我正在使用Z3和扩展的SMT-LIB2语法来解决我的horn子句。我知道horn子句的头应该是未解释的谓词；但是，我不知道如何将以下子句重写为一组horn子句。

(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)不能是horn子句的开头。我可以将最后一个子句重写如下：

(rule (=> (and (inv  a k) (> k 0) ) (gtz a)))
(rule (=> (> a 0) (gtz a)))

但是，子句变得如此微弱，以至于我无法获得不变式inv的预期模型。我想知道是否有更好的方法可以做到这一点。

Answer 1

也许你想说

(declare-rel inv (Int Int ))
(declare-rel q ())
(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) (not (> a 0))) q))
(query q )