使用SMT2 / Z3的谓词

Question

我需要使用SMT2 / Z3写下以下句子，不确定是否有区别。

对于每个有父母的人，他/她必须爱他/她的父母。

到目前为止，我已经写过

(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(declare-fun love () Bool)
      (assert =>
         ((forall (x) (y x) )
         (exists z)))

(check-sat)

但这只是给我一个似乎无法解决的参数错误。

我的谓词是

Person（x）x是一个人。

Parent（x，y）x是y的父母。

[爱（x，y）x爱y。

非常感谢任何帮助。

Answer 1

这里是一种方式：

(declare-sort Person 0)
(declare-fun parentOf (Person Person) Bool)
(declare-fun loves    (Person Person) Bool)

(assert
   (forall ((x Person) (y Person))
       (=> (parentOf x y)
           (loves x y))))

(check-sat)
(get-model)

z3说：

sat
(model
  ;; universe for Person:
  ;;   Person!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun Person!val!0 () Person)
  ;; cardinality constraint:
  (forall ((x Person)) (= x Person!val!0))
  ;; -----------
  (define-fun loves ((x!0 Person) (x!1 Person)) Bool
    false)
  (define-fun parentOf ((x!0 Person) (x!1 Person)) Bool
    false)
)

从本质上讲，z3告诉我们我们的约束是可满足的（这是输出sat的含义），并且a（注：not the）满足赋值是一个宇宙，其中有：

• 正好一个人，名为Person!val!0
• 没人爱任何人
• 没有人是其他任何人的父母

显然可以满足所有约束条件，但也许不是最有趣的模型。如果您进一步主张事实，则可以得到更丰富的模型。 （例如，您可以说至少有5个人，没有人是他们自己的父母，养育关系不对称，每个人都爱自己，等等，具体取决于您要建模的对象。）

请记住，SMT求解器不适用于处理量词。尽管这样的语句可以很好地工作，但是大量使用量词和一阶逻辑会将理论置于半确定的范围内，即z3最终可以说unknown。 SMT求解器最适合于无量纲的理论组合，例如算术，数组，数据类型等。对于此类问题，Prolog可能是您进行建模的最佳选择。