如何在Z3Py中验证axiom？

Question

我不熟悉Z3，但我知道公理是一个假设的前提，不管它是否明显，它被用来证明其他命题

我试图定义一个结合Z3Py的方法长度和包含的公理，我的想法的一个例子是：

lista = Const('lista', SeqSort(IntSort()))

a, b = Ints('a b')
solve(ForAll(lista, Length(lista)> 3))

这段代码会被认为是一条公理吗？这让我回想起“没有解决办法”，我不明白为什么。它应该支持两个元素的列表吗

Answer 1

这个问题很令人困惑，根本不清楚你在问什么。一个公理通常是一个量化的陈述，即在它里面有Forall和/或Exists的东西。下面是一个从https://ericpony.github.io/z3py-tutorial/advanced-examples.htm复制的示例：

f = Function('f', IntSort(), IntSort(), IntSort())
x, y = Ints('x y')
print ForAll([x, y], f(x, y) == 0)
print Exists(x, f(x, x) >= 0)

a, b = Ints('a b')
solve(ForAll(x, f(x, x) == 0), f(a, b) == 1)

如您所见，公理通常用于表示未解释函数的属性：f在上面的示例中

你的描述很难理解，但听起来你可能有XY问题：http://xyproblem.info/看看你是否能用你想要达到的目标来重新表述这个问题，而不是做出假设！（很抱歉说了双关语！）祝你好运

关于您的编码：

让我们关注一下您所写的内容：

solve(ForAll(lista, Length(lista)> 3))

这里您要说的是，对于所有列表（您命名为^{），它们的长度都大于3。你用更数学的符号表示：

∀x. length (x) > 3

这显然不是真的，因为您可以将空列表作为反例

一般来说，公理将创建一个新的未解释的排序和/或未解释的函数及其状态属性。你已经表示你是一个新用户，很可能在这个级别上你不需要任何实用的公理。当您就特定主题提出非常具体的问题时，Stack overflow的效果最好，所以请随意提出不同的问题