问题标签 [quantifiers]

懒惰和贪婪的想法很容易理解，但我只*+在我的正则表达式（在 Java 中）[A]|[^B]*+(?!C)（A、B、C 是任意值）中看到/使用过一次，因为它在懒惰修饰符导致 StackOverflow 错误时起作用。

由于大多数搜索引擎无法搜索符号，我找不到任何关于此的文档。那么 *+ 究竟做了什么以及它是如何做到的呢？

我要求 Z3 使用 SMTLIB 2 接口在 UFLIA 理论中进行量词消除。所以我断言了一个包含 21 个存在量化变量的公式，其中 7 个是整数，14 个是布尔值。然后我这样做(apply qe)，Z3 返回一个目标，该目标仍然包含九个存在量化变量，(x!1 Int)named(x!14 Int)和(x!14!1 Int)to (x!14!7 Int)。这是否意味着该qe策略不会一次消除所有量词？

如果我做(assert qe)两次，除了重命名的量化变量之外，目标保持不变。我试过(repeat qe)了，但是返回unsupported，也将:eliminate-variables-as-block参数设置为 true 不会改变任何东西。

但是，如果我从目标中获取量化公式，自行断言并assert qe再次执行，Z3 会按照我的意愿消除剩余的量词。

请参阅下面的链接以获取公式，我需要做一些魔术来让 Z3 一次消除所有量词吗？

https://gist.github.com/chsticksel/edeb350fa4474713f3df#file-apply-qe-does-not-eliminate-all-quantifiers-at-once-smt

我想证明以下定理

有上下文

该陈述在谓词逻辑中似乎是正确的，但我不知道如何证明它。问题本质上是我不能一次消除所有的 forall，但我不能在破坏假设 H 之前既不向左也不向右应用。

有没有一种简单的方法可以做到这一点？

我有以下定理要证明：

分手后

第一个含义很简单，基本上我们必须在存在量词中使用从forall引入的x

但另一方面我不能这样继续下去，我认为应该有一个我找不到的想法。有什么建议吗？

另一个艰难的目标（当然对我来说）如下：

我完全不知道我能做什么。如果我引入一些东西，我会在假设中得到一个全称量词，然后我不能用它做任何事情。

我想它存在管理这种情况的标准方法，但我无法找到它。

我正在尝试增加FOL.thy量词MOST，我打算将其定义为简单多数，即

我不确定如何修改FOL.thy文件。在下axiomatization，我想补充：

并且，在该where条款下：

其中“...”是表达上述约束的正确方式，即P(x)和的基数~P(x)。（同样，我不确定这里有一个好名字，欢迎提出建议。）

我想在“符号”部分添加一个条目，并且由于缺乏更好的想法，选择使用 delta：

同样在该notation部分中。

1）如何正确表达基数约束？

2）我还需要修改哪些其他内容？

对于后一个问题，指出最终我想评估一些不同的结论是否是必要的、可能的或不可能的可能会有所帮助，假设前提将包括使用“大多数”和“全部”的量化断言（以及连词、析取等）。

I have a multiclass problem for which i want to predict the quantification using Weka (SVMs regression etc). I am a new in regression methods. So far I did regression of single class in Weka because I do not know how to provide continuous outputs for multiclass problem. Should I use individual regression model for each class? Is there any method to do simultaneous regression for each class. (my each individual class have same range of of continuous outputs...so can not differentiate if I put all four (say) class simultaneously in a .csv file as input)..

Thanks in Advance...

我有一个简单的公式，在数组集上带有量词，Z3(4.3.2) 返回“未知”。

详细的是：

似乎 Z3 允许这种公式。由于我对冗长的不完全理解，我是否错过了一些可以使用的策略？你能帮忙解决这个公式吗？

我在 SO 上发现了一个类似的问题，但我无法理解。这就是我需要的；

6 位或更多位，允许使用这些字符\s\-\(\)\+

这就是我所拥有的/^[0-9\s\-\(\)\+]{6,}$/

问题是，除了数字之外，我不希望任何其他内容计入 6 个或更多量词。我怎样才能只“计算”数字？如果我可以阻止其他允许的字符被相邻输入，那也很好，例如：

经过一个小时的阅读和查看正则表达式备忘单后，我希望有人能指出我正确的方向！

在页面的末尾，试图解释贪婪、不情愿和占有量词是如何工作的： http: //docs.oracle.com/javase/tutorial/essential/regex/quant.html

但是我尝试了一个例子，但我似乎并不完全理解它。

我将直接粘贴我的结果：

为什么第一个reg.exp。找不到匹配项，而第二个匹配项呢？这两个 reg.exp. 之间的确切区别是什么？