1

我正在使用 Z3 来解决我的角子句。在 Horn 子句的主体中，未解释的谓词应该是肯定的。但是，我需要否定一些未解释的谓词。

我已经看到了一些否定工作正常的例子。例如 Z3 将返回sat以下示例：

(set-logic HORN)
(declare-fun inv (Int) Bool)

(assert (inv 0))
(assert (forall ((k Int)) (or (> k 10) (not (inv k)) (inv (+ k 1)))))
(check-sat)

但我的示例如下所示，Z3 返回unknown.

(set-logic HORN)
(declare-fun inv (Int  ) Bool)
(declare-fun s ( Int ) Bool)

(assert (forall ((k Int) (pc Int))(=>(and  (= pc 1)(= k 0))  (inv k ))))

(assert (forall ((k Int)(k_p Int)(pc Int)(pc_p Int))
  (=>(and  (inv k )(= pc 1)(= pc_p 2)(= k_p (+ k 1))(not (s pc ))(s pc_p ))  
(inv  k_p ))))

(check-sat)

我想知道是否有办法将我的子句重写为 Z3 的 Horn 子句片段。

4

1 回答 1

1

您的子句不在 Horn 片段中，因为谓词 s 在最后一个断言中与两个极性一起使用。因此，有两次出现具有正极性的谓词（（s pc）和（inv k_p）都是正极性）。避免极性问题的一个基本方法是为 s 类型的 Bool 引入一个额外的参数。因此，您还必须使用 Horn 子句说明 s 的规范是什么，所以这一切都说得通。典型的场景是 s 对递归过程的行为进行编码，并且 s 的额外布尔参数将是过程 s 的返回值。当然，这种编码并不能确保 s 是完全的或功能性的。还有第二种方法，即在“inv”中添加一个额外的参数，让 's' 成为一个数组。然后出现次数 (not (s pc)) 变为 (not (select s pc)),

于 2019-12-08T13:24:20.073 回答