Z3:定义类层次结构的更方便和有效的方法是什么? [英] Z3: what's a more convenient and efficient method for defining class hierarchies?

问题描述

作为之前与 Z3 相关的问题的扩展 使用分辨率定理证明 Z3 并建立在 @alias 之上在 https://stackoverflow.com/a/62721185/13861050

As an extension to a previous Z3-related question Using Resolution theorem proving with Z3 and built on top of @alias 's answer at https://stackoverflow.com/a/62721185/13861050

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

I've added a few more functions and relations:

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 是一个函数.

So my question is: Is there a shorter (but still performant / computationally efficient) way of specifying hierarchical relations such as s.add(ForAll([x], Implies(ANIMAL(x), LIVING_THING(x)))). I mean something like s.add(LIVING_THING(ANIMAL)) which currently doesn't work because the argument ANIMAL is a function.

此外，我想为某些函数指定某些属性，例如对称(作为更基本的情况).我已经定义:

Also, I'd like to specify certain properties to some functions such as being symmetric (as a more basic case). I've defined:

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 是对称的.那么是否有一种更优雅的方式来指定函数列表的对称属性(以及将来的许多其他此类元属性)，例如类似:

The last two constraints basically mean that both the functions SAMEWEIGHT, isMarriedTo and loves are symmetric. So Is there a more elegant way of specifying the symmetric property (and in the future, many other such meta properties) for a list of functions, e.g. something like:

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

1. SymmetricFunctionType is defined by ForAll([x, y], Implies(SymmetricFunctionType(x, y), SymmetricFunctionType(y, x)))
2. the functions SAMEWEIGHT, isMarriedTo and loves, etc. belong to the class SymmetricFunctionType. In other words what's the idiomatic way of doing that in Z3?

推荐答案

SMTLib 本质上是一阶逻辑.(更准确地说，这是一个一阶多排序逻辑.)

SMTLib is essentially a first-order logic. (More precisely, it's a first-order many-sorted logic.)

这几乎不允许任何将函数作为参数的构造.所以，你不能写出这个函数是对称的"的属性；或 LIVING_THING(ANIMAL) 形式的二阶语句，其中 ANIMAL 是一个函数.

This pretty much disallows any construct that takes functions as arguments. So, you cannot write properties that say "this function is symmetric" or second order statements of the form LIVING_THING(ANIMAL) where ANIMAL is a function.

对于大多数实际目的，这不会施加太多限制.请记住，SMTLib 并不是真的要手写:它通常用作中间语言:一些更高级别的前端生成 SMTLib 并将结果翻译回来，随着它的进展生成它需要的所有实例.多态性也是如此:你不能编写一致"的函数.例如，处理不同种类的工作.您必须为您需要的每个案例编写一个单独的实例.(这通常称为单态化过程.)

For most practical purposes, this doesn't impose too much of a restriction. Keep in mind that SMTLib is not really intended to be hand-written: It's usually used as an intermediate language: Some higher-level front-end generates SMTLib and translates results back, generating all the instances it needs as it makes progress. The same thing is true for polymorphism: You cannot write functions that "uniformly" work over different sorts, for instance. You have to write a separate instance for each case you need. (This is usually known as the process of monomorphisation.)

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

Another important point to make is that while SMTLib does allow quantifiers, the decidable fragment is usually the quantifier-free subset of combinations of logics. Once you throw quantifiers in, it's more likely that you'll start getting unknown answers. If you want to reason with quantifiers, you're better off using a proper theorem prover like Isabelle, Coq, etc., all of which allow SMTLib as an engine that you can call to discharge goals.

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

Note that there's a new version of SMTLib that's currently being developed, which will include higher-order features directly in the language. In particular, the core logic will move to simply-typed higher-order logic, from the current many-sorted first-order logic. (Details: http://smtlib.cs.uiowa.edu/version3.shtml). Of course, this is a relatively new development, and it'll be a while before the standard settles and solvers start supporting these new features in a consistent way. So, some of what you are trying to do might indeed be possible in the (somewhat) near future. Currently, your only option is to create instances separately.

这篇关于Z3:定义类层次结构的更方便和有效的方法是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！