Z3：定义类层次结构有什么更方便高效的方法？答案

【问题标题】：Z3: what's a more convenient and efficient method for defining class hierarchies?Z3：定义类层次结构有什么更方便高效的方法？
【发布时间】：2020-07-04 06:08:14
【问题描述】：

作为对先前 Z3 相关问题 Using Resolution theorem proving with Z3 的扩展，并建立在 @alias 在 https://stackoverflow.com/a/62721185/13861050 的答案之上

我又添加了一些函数和关系：

FEMALE              = Function('FEMALE',            Thing,        BoolSort())
ANIMAL              = Function('ANIMAL',            Thing,        BoolSort())
LIVING_THING        = Function('LIVING_THING',        Thing,        BoolSort())
ENTITY              = Function('ENTITY',        Thing,        BoolSort())

s.add(ForAll([x], Implies(WOMAN(x), FEMALE(x))))
s.add(ForAll([x], Implies(LIVING_THING(x), ENTITY(x))))
s.add(ForAll([x], Implies(ANIMAL(x), LIVING_THING(x))))
s.add(ForAll([x], Implies(WOMAN(x), ANIMAL(x))))

所以我的问题是：是否有一种更短（但仍然高效/计算高效）的方式来指定层次关系，例如s.add(ForAll([x], Implies(ANIMAL(x), LIVING_THING(x))))。我的意思是像 s.add(LIVING_THING(ANIMAL)) 这样的东西，它目前不起作用，因为参数 ANIMAL 是一个函数。

另外，我想为某些函数指定某些属性，例如对称（作为更基本的情况）。我已经定义了：

isMarriedTo = Function('isMarriedTo',            Thing, Thing,  BoolSort())
loves       = Function('loves',            Thing, Thing,  BoolSort())

s.add(ForAll([x, y], Implies(SAMEWEIGHT(x, y), SAMEWEIGHT(y, x))))
s.add(ForAll([x, y], Implies(isMarriedTo(x, y), isMarriedTo(y, x))))
s.add(ForAll([x, y], Implies(loves(x, y), loves(y, x))))

最后两个约束基本上意味着函数SAMEWEIGHT、isMarriedTo 和loves 都是对称的。那么是否有一种更优雅的方式来指定函数列表的对称属性（以及未来的许多其他此类元属性），例如类似：

SymmetricFunctionType 由ForAll([x, y], Implies(SymmetricFunctionType(x, y), SymmetricFunctionType(y, x))) 定义
函数SAMEWEIGHT、isMarriedTo和loves等属于SymmetricFunctionType类。换句话说，在 Z3 中这样做的惯用方式是什么？

【问题讨论】：

标签： python c++ z3

【解决方案1】：

SMTLib 本质上是一个一阶逻辑。（更准确地说，它是一阶多排序逻辑。）

这几乎不允许任何将函数作为参数的构造。因此，您不能编写“此函数是对称的”属性或LIVING_THING(ANIMAL) 形式的二阶语句，其中ANIMAL 是一个函数。

对于大多数实际目的，这不会施加太多限制。请记住，SMTLib 并不是真正打算手写的：它通常用作中间语言：一些更高级别的前端生成 SMTLib 并将结果翻译回来，在它取得进展时生成它需要的所有实例。多态性也是如此：例如，您不能编写“一致地”在不同类型上工作的函数。您必须为您需要的每个案例编写一个单独的实例。（这通常被称为单态化过程。）

另一个重要的一点是，虽然 SMTLib 确实允许量词，但可判定片段通常是逻辑组合的无量词子集。一旦你加入量词，你更有可能开始得到unknown 的答案。如果你想用量词推理，你最好使用像 Isabelle、Coq 等合适的定理证明器，所有这些都允许 SMTLib 作为一个引擎，你可以调用它来实现目标。

SMTLib v3

请注意，目前正在开发新版本的 SMTLib，它将直接在语言中包含高阶功能。特别是，核心逻辑将从当前的多排序一阶逻辑转移到简单类型的高阶逻辑。（详情：http://smtlib.cs.uiowa.edu/version3.shtml）。当然，这是一个相对较新的发展，标准制定和求解器开始以一致的方式支持这些新功能还需要一段时间。所以，你正在尝试做的一些事情在（有点）不久的将来可能确实是可能的。目前，您唯一的选择是单独创建实例。

【讨论】：