问题标签 [theorem-proving]

定理证明工具 z3 需要花费大量时间来解决一个公式，我相信它应该能够轻松处理。为了更好地理解这一点并可能优化我对 z3 的输入，我想查看 z3 在其求解过程中生成的内部约束。从命令行使用 z3 时，如何打印 z3 为其后端求解器生成的公式？

我对使用通用量词和 declare-const 而不使用 forall 感到有些困惑

我可以这样写：

在这两种情况下，Z3 将探索 Int 类型的所有可能值。那么有什么区别呢？我真的可以使用 declare-const 来消除 forall 量词吗？

我正在试验 Z3，我结合了算术、量词和相等的理论。这似乎不是很有效，事实上，在可能的情况下用所有实例化的地面实例替换量词似乎更有效。考虑以下示例，其中我为一个函数编码了唯一名称公理，该函数f接受两个 sort 参数Obj并返回一个解释的 sort S。这个公理表明每个唯一的参数列表都f返回一个唯一的对象：

尽管这是在逻辑中定义这样一个公理的标准方法，但像这样实现它在计算上是非常昂贵的。它包含 4 个量化变量，每个变量可以有 8 个值。这意味着这会导致8^4 = 4096平等。这需要 Z3 0.69s 和 2016 量词实例化来证明这一点。当我编写一个生成此公式实例的简单脚本时：

生成这些公理需要 0.002 秒，在 Z3 中证明它需要 0.01 秒（或更少）。当我们增加域中的对象或函数的参数数量时，f这种差异会迅速增加，量化的情况很快就会变得不可行。

这让我想知道：当我们有一个有界域时，为什么我们首先要在 Z3 中使用量词？我知道 SMT 使用启发式方法来寻找解决方案，但我觉得它仍然无法与一个简单的特定领域接地器在效率上竞争，后者将接地实例提供给 SMT，这只不过是 SAT 解决方案。我的直觉正确吗？

我正在尝试使用 Z3（Microsoft Research 开发的 SMT 求解器）检索某些一阶理论的所有可能模型。这是一个最小的工作示例：

在这个命题情况下，有两个令人满意的分配：f->true和f->false。因为 Z3（以及一般的 SMT 求解器）只会尝试找到一个令人满意的模型，所以不可能直接找到所有解决方案。在这里我找到了一个有用的命令叫做(next-sat)，但是Z3的最新版本似乎不再支持这个。这对我来说有点不幸，总的来说我认为该命令非常有用。还有另一种方法吗？

我正在尝试使用Skolemization删除我的理论中的存在量词。这意味着我用存在量词范围内的普遍量化变量参数化的函数替换存在量词。

在这里，我找到了如何在 Z3 中执行此操作的说明，但我仍然无法执行此操作。假设有以下两个函数：

我相信这f2应该是正确的，因为存在一个t这样的整数(f1 t)是正确的，即t=3。我通过为存在量化公式引入一个常数来应用 Skolemization：

然后将存在量词的公式改写为：

这不起作用，也就是说，常数c没有值 3。我怀疑这是因为我们没有对常数给出解释c，因为如果我们添加(assert (= c 3))它可以正常工作，但这会消除存在主义的整个想法量词。有没有一种方法可以让我给出一个不太明确的解释，c这样才能奏效？

我正在尝试使用 C API 生成 Craig 插值，但得到的结果不正确。但是，当我通过 Z3_write_interpolation_problem 将相同的问题转储到文件并调用 iZ3 时，我得到了预期的插值。

我附上代码以便能够重现相同的结果。我正在使用 z3 4.1

我使用以下命令生成可执行文件：

g++ -fopenmp -o 插值插值.c -I/home/jorge/Systems/z3/include -I/home/jorge/Systems/z3/iz3/include -L/home/jorge/Systems/z3/lib -L/主页/jorge/Systems/z3/iz3/lib -L/home/jorge/Systems/libfoci-1.1 -lz3 -liz3 -lfoci

请注意，约束基本上是：

A = (x=0 and x1 = x0+2 and x2 = x1 + 2),

和 B = (x2 > 10)

这显然是不满意的。此外，很容易看出唯一的公共变量是 x2。因此，任何有效的插值只能包括 x2。

如果我运行可执行文件 ./interpolation 我会得到无意义的插值：

但是，如果我运行“iz3 tmp.smt”（其中 tmp.smt 是使用 Z3_write_interpolation_problem 生成的文件），我将获得一个有效的插值：

未饱和插值：(<= x2 10)

这是一个错误吗？还是我在调用 Z3_interpolate 时遗漏了一些重要的先决条件？

PS 我找不到任何使用 iZ3 和 C API 的示例。

干杯，豪尔赫

我需要对数组的长度进行建模。所以我声明了一个函数

同时，我想定义一些使用define-fun.

但是，当我在 Z3 上进行了一些测试时，似乎define-fun并declare-fun不能存在于同一个源文件中？

如下代码可以正常工作：

（来源：http ://rise4fun.com/Z3/jRzs ）

但是下面，不管LEN插入到哪里，都会出现错误：

（来源：http ://rise4fun.com/Z3/HdEy ）

有人知道如何解决这个问题吗？

我正在为 OTTER 编写一个非常简单的输入文件：

我得到这个搜索输出：

为什么 OTTER 不推断Causes($c2,$c1)？

编辑：我删除了方括号[Nipah(x) & Encephalitis(x)]，它起作用了。为什么这很重要？

我正在尝试优化使用 Z3 来证明有关一阶理论的事实。目前，我在 Python 中指定了一个一阶理论，将量词固定在那里，并将所有子句连同证明目标的否定一起发送到 Z3。我有以下想法，希望可以优化结果：我只想将与证明目标相关的理论公式发送到 Z3。我不会详细讨论这个概念，但我认为直觉很简单：我的理论是公式的合取，我只想发送可能影响证明目标真值的合取。

我的问题是：这是否会导致效率的提高，或者 Z3 是否已经使用了类似的方法？我猜不会，因为我不认为 Z3 总是假设最后一个断言是证明目标，所以它没有办法对此进行优化。

我对 Coq 还很陌生，正在尝试来自 Ruth 和 Ryan 的示例引理。使用自然演绎的证明非常简单，这就是我想用 Coq 证明的。

我被困在第 3 行assume p。

有人可以告诉我从自然演绎到 Coq 关键字是否存在一对一的映射？