Z3：定义class层级有什么更方便有效的方法？

Question

作为对先前 Z3 相关问题的扩展 and built on top of @alias 's answer at

我添加了更多函数和关系：

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等函数属于classSymmetricFunctionType。换句话说，在 Z3 中惯用的方式是什么？

Answer 1

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

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

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

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

SMTLib v3

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

Z3：定义class层级有什么更方便有效的方法？

Z3: what's a more convenient and efficient method for defining class hierarchies?

c++

python

z3

SMTLib v3