具体来说，我正在研究一阶阵列理论中不同的可判定碎片.
例如，第1篇文章给出了一个数组的∃∗∀∗片段，我们可以证明它的属性:例如，∀i . 0 ≤ i < n → a[i+1] = a[i]−1。然而，通过定义一种新的带计数器的Büchi自动机类，他们按照自动机理论方法建立了这种逻辑的可判定性。对于我来说，这听起来远不是我所理解的SMT求解器作为可判定理论与量词的决策过程所实现的经典量词消除。因此，我的问题是:如果一个理论可以像第1篇那样被证明是可判定的，那么Z3 (和其他求解者)是否实现了这些决策过
浏览 8提问于2022-10-05得票数 0
回答已采纳
1回答
自由双笛卡尔闭范畴(BCCC)的决策问题是可判定的吗？等价地，对于具有强n值积和和的简单类型lambda演算，等式可判定吗？对于免费的几乎BCCC的决策问题是可以确定的：
但这项工作不包括初始对象，也不包括空类型的lambda-calulus术语，尽管他们推测他们的方法可以扩展到BCCCs。
浏览 0提问于2013-09-18得票数 1
我的问题:定义单词的两个集合P和q(即两个问题)：P是不可判定的和不半可的，q是不可判定的和半可判定的，P是⊂q的。
浏览 1提问于2015-02-22得票数 1
回答已采纳
2回答
最近，我被要求检查一行代码中的数组是否为空。int[] array = new int[5];你能帮我找一个单行代码来检查它是空的还是不空的？
浏览 1提问于2016-04-01得票数 1
我正在尝试创建一个算法来决定以下可判定问题:给定一个CFG H，to⇒*ε。也就是说，H可以在任意数量的步骤中生成空词。算法必须是可判定的，这意味着它总是正确地在所有输入上停止。
浏览 13提问于2019-12-04得票数 2
我的第一个问题是，我是否可以用Z3Py表示以下公式：这意味着:数组中是否存在一个位置i::0<i<|arr|，其值a[i]大于数组avg(arr)的平均值加上给定的阈值t。我的第二个问题是: Z3中涉及数组的可判定片段的表达能力如何？我阅读了关于数组的全部理论是如何不可判定的()，而只是一个具体的片段，数组属性片段。
浏览 8提问于2022-09-19得票数 0
回答已采纳
我目前正在使用Python + Mechanize从本地服务器检索页面。如您所见，代码使用"localhost“作为代理。该代理是Fiddler2调试代理的实例。这完全符合预期。这表明我的机器可以访问test_box。import mechanize
browser = mechanize.Browser();
browser.set_proxies({"http": "127.0.0.1
浏览 0提问于2013-03-06得票数 2
回答已采纳
我正在运行一个简单的判定器pollForDecisionTask循环。但是当Amazon的最后一个事件类型是DecisionTaskCompleted时，它就被卡住了。我的意思是，反应很好，但taskToken是空的！！有线索吗？我重新检查了taskList和域名，但什么也没成功。
浏览 5提问于2012-10-10得票数 1
回答已采纳
2回答
我有一个php数组这里是我的php代码$data = array('A','B','C','D','E','F');for($k = 0;$k<$count;$k++){
foreach
浏览 10提问于2014-07-07得票数 0
回答已采纳
给定一个非空字符串 s 和一个包含非空单词的列表 wordDict，判定 s 是否可以被空格拆分为一个或多个在字典中出现的单词。说明：拆分时可以重复使用字典中的单词。你可以假设字典中没有重复的单词。
浏览 78提问于2021-10-15
1回答
我知道$E_{LBA}$ = {< M>| L(M) = \emptyset }$是一种不可判定的语言，但它也是可识别的吗？
浏览 1提问于2016-12-14得票数 2
1回答
SMT-LIB中的QF_NRA逻辑是可判定的吗？
我知道Tarski证明了非线性算法是可判定的，在实数中多项式系统是可判定的。然而，QF_NRA是否属于这一保护伞并不明显，因为QF_NRA包含除法。如果零除法不是QF_NRA的一部分，那么QF_NRA中的除法就可以转换为乘法，这个问题将如Tarski所证明的那样是可判定的。如果QF_NRA中实际上包含了部门，那么我就不太确定了。在这种情况下，QF_NRA仍然是可判定的。
浏览 2提问于2016-10-21得票数 2
回答已采纳
问题是关于静态方法Objects.deepEquals类(自Java 7以来)： if (a == b) else if (a == null || b == null) else}
浏览 4提问于2015-12-30得票数 16
回答已采纳
2回答
这不是PHP的最大执行时间，因为设置的时间足够长。
这是我的VPS提供者为了对抗负载而做的事情，还是Ubuntu为了保持系统响应而做的事情？根据munin的说法，我的VPS配置得很奇怪。
浏览 0提问于2011-05-28得票数 2
1回答
∀Y.Φ(X,Y)形式的企业家量化公式集，其中X和Y是(可能是空的)变量序列。量化的顺序，即∃*∀*，是否关系到EPR的可判定性？如果转换量化顺序，我们是否失去了决策能力？特别是，我对在可判定逻辑中捕获集一元绑定操作的语义感兴趣。然而，当我在Z3上使用这样的公式时，我从来没有遇到过超时问题，我不知道上面的公式是否确实处于某种可判定的片段中(同时也承认在实践中的可解性并不意味着理论上的可判定性)。欢迎任何意见。
浏览 5提问于2017-09-12得票数 3
回答已采纳
我的意思是，我想这个组合理论是半可判定的(因为量化词和序列)，但是我们能把它形式化吗？如果是的话，我想(以正确的方式)结合这些理论，但我不知道如何。一个练习(作为一个方向)现在，假设我想向它添加一个avg函数。，，我必须以某种方式将数组属性片段与某种递归函数理论和整数理论结合起来吗？我该怎么做？注意，这些理论涉及到quantifiers.Do，我必须首先将这
浏览 6提问于2022-09-27得票数 0
回答已采纳
3回答
C#静态数组绑定检查
、、、、
是否有用于C#的工具可以静态地(不执行代码)检测出绑定数组访问，即将抛出的数组访问。
谢谢。编辑:是的，我知道在general 中，理论上是不可能这样做的(也就是说，它是不可判定的)，但这并不意味着在某些情况下不可能这样做(事实上，正式验证的整个领域是为理论上不可能的事情生产实用工具)。
浏览 6提问于2013-12-06得票数 1
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
云直播
对象存储
腾讯会议活动推荐
腾讯云开发者
