使用SMT2 2/Z3的谓词句
使用SMT2 2/Z3的谓词句
提问于 2020-01-16 19:28:36
我需要用SMT2 2/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是人。
父(x，y) x是y的父。
爱(x，y)爱y
任何帮助都非常感谢。
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-01-16 21:27:28
有一种方法：
(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 )--满意的任务是这样一个宇宙：
Person!val!0
- Nobody anyone
- Nobody
- 正是一个人，他是其他人
的父亲
它显然满足了所有的约束条件，但也许并不是最有趣的模型。如果你坚持进一步的事实，你可以得到更丰富的模型。(例如，你可以说至少有5个人，没有人是他们自己的父母，父母关系不对称，每个人都爱自己，等等，这完全取决于你想要做什么。)
请记住，SMT求解器不适合处理量词。虽然像这样的陈述会很好，但量词和一阶逻辑的广泛使用将把理论应用到半可判定的领域，也就是说，z3可能最终会说unknown。SMT求解器对于算术、数组、数据类型等理论的无量词组合是最好的。对于这样的问题，Prolog可能是您建模目的的最佳选择。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/59776535
复制相关文章
相似问题
腾讯云开发者
