问题标签 [quantifiers]

我想将公式中的所有嵌套量词拉到最外层。我希望以下命令可以在 Z3 中工作，但它们不能：

目的是:pull-nested-quantifiers什么？如何使用 SMT-LIB 或 Z3 API 提取嵌套量词？

我正在尝试使用 Z3 对集合中元素的包含和排除进行建模。特别是包含具有不同值的元素，并排除尚未在目标集中的元素。所以基本上我想要一个集合 U 并让 Z3 找到一个集合 U_d ，它只包含具有不同值的 U 元素。

我当前的方法使用量词，但我无法理解如何声明如果元素出现在 U_d 中，我希望始终将它们包含在 U_d 中。

它产生的作业是：

我想要的作业是：

我知道将 false 分配给 A 和 B 在逻辑上是正确的分配，但我不知道如何以排除这些情况的方式陈述事情。

也许我没有正确考虑这个问题。

任何建议将不胜感激。:)

Haskell Wiki很好地解释了如何使用存在类型，但我不太了解它们背​​后的理论。

考虑这个存在类型的例子：

为我们可以转换为String. wiki 提到我们真正想要定义的类型是

即一个真正的“存在”类型——我松散地认为这是在说“数据构造函数S采用任何存在Show实例的类型并包装它”。实际上，您可能可以编写如下 GADT：

我没有尝试编译它，但它似乎应该可以工作。对我来说，GADT 显然等同于我们想要编写的代码 (2)。

但是，我完全不明白为什么（1）等于（2）。为什么将数据构造函数移到外面会forall变成一个exists？

我能想到的最接近的是逻辑中的德摩根定律，其中交换否定和量词的顺序将存在量词变成全称量词，反之亦然：

但数据构造函数似乎与否定运算符完全不同。

forall使用而不是不存在来定义存在类型的能力背后的理论是什么exists？

我正在尝试使用 Z3 .net API 来获取存在量词 expr。以下是我的代码：

'

对于该程序，我得到以下结果：

我的问题是 1. 是什么意思！在结果中/ 2. 我无法获得SAT成绩的原因是什么？3. 除了Z3网站上的API菜单外，谁能提供一些与Z3 .NET API对应的武术。

非常感谢！

除了 Z3 之外，是否还有其他可用（并且仍然受支持）的 SMT 工具可以为线性整数算术执行量词消除？

谢谢。

我试图让 Z3 验证一些在符号中使用迭代最大值的正式证明。例如，对于 fa 函数 (↑i: 0 ≤ i < N: f(i)) 指定 f 在应用于 0 和 N 之间的值时的最大值。它可以很好地公理化为：

(↑i: p(i): f(i)) ≤  x <=> (∀i: p(i): f(i) ≤ x)

在 i 的类型上使用 pa 谓词。有没有办法在 Z3 中定义这样的量词？

制定我的证明非常方便，所以我想尽可能地接近这个定义。

谢谢！

可能重复：
Python 正则表达式 - 如何从通配符表达式中捕获多个组？
组匹配的python正则表达式

我知道有更好或更简单的方法可以做到这一点，但是当我自己尝试过但没有奏效时，我很感兴趣为什么，所以这里有问题：

假设我想使用正则表达式获取 Xml 属性。让我们看看下面的 XML-Node：

解析Node以及OtherNode我有以下正则表达式：

的输出pattern.findall(xml)是：

('Node', 'key2="val2"', 'key2', 'val2') ('OtherNode', '', '', '')

和输出[m.groupdict() for m in pattern.finditer(xml)]：

似乎只有最后一个元变量可以作为组访问。

如何搭配key1以及key2？是否可以将多个组与(...)*构造匹配？换句话说：meta如果存在，我希望正则表达式多次匹配命名组。

好的，我有给定的关系：如果 F(x) 不正确，则没有任何情况满足 G(x) 和 H(y,x)。((∀x ¬F(x)) ⇒¬(∀y G(y) ˄ H(y,x)))

现在，我可以将其转换为： (∀y G(y) ˄ H(y,x))) ⇒ ((∀x F(x)) ????

如果不是，则左侧基本上必须暗示：如果 F(x) 不正确.... 没有提及 For All 或 Existential 量词。我可以把否定放在量词之外，即把它写成 (¬(∀x F(x))，因为这让工作更容易？？？

我想使用 Z3 通过 C/C++ API 消除线性整数算术公式中的量词。考虑一个简单的例子：Exists (x) (x <= y & y <= 2*x)。具有相同模型的无量词公式是 y >= 0。

我试着这样做：

我得到的是

(存在 ((x Int) (and (<= xy) (<= y (* 2 x))))

而我想获得类似的东西

(<= 0 年)

Z3有可能获得它吗？提前谢谢了。

我想修剪一个字符串，如果它以 foo 或 bar 开头和/或结尾，并且想要获取正则表达式组中的内部字符串。
例如

“fooTestbar”应该是“Test”，
“Test2bar”应该是“Test2”
，“Test3”应该是“Test3”。

我目前的正则表达式是：

但这不起作用，因为我无法将量词?应用于替代组（(foo|bar)）。

我的代码

任何帮助将不胜感激。