腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
1
回答
Z3 (和其他求解者)总是在可能的情况下使用终止决策过程吗?
arrays
、
z3
、
smt
、
theorem-proving
、
first-order-logic
具体来说,我正在研究一阶阵列理论
中
不同的可
判定
碎片. 例如,第1篇文章给出了
一个
数组
的∃∗∀∗片段,我们可以证明它的属性:例如,∀i . 0 ≤ i < n → a[i+1] = a[i]−1。然而,通过定义一种新的带计数器的Büchi自动机类,他们按照自动机理论方法建立了这种逻辑的可
判定
性。因此,我的问题是:如果
一个
理论可以像第1篇那样被证明是可
判定
的,那么Z3 (和其他求解者)是否实现了这些决策过程?换句话说,∀i . 0 ≤ i < n → a[i+1
浏览 8
提问于2022-10-05
得票数 0
回答已采纳
1
回答
对于Z3(Py)
中
的
数组
,我们能有多大的表达能力?
一个
例子
arrays
、
z3
、
z3py
、
theorem-proving
、
dafny
我的第
一个
问题是,我是否可以用Z3Py表示以下公式:这意味着:
数组
中
是否存在
一个
位置i::0<i<|arr|,其值a[i]大于
数组
avg(arr)的平均值加上给定的阈值t。我知道这种表达式可以在Dafny
中
查询,而且(因为Dafny在下面使用Z3 ),我想这可以在Z3Py
中
完成。 我的第二个问题是: Z3
中<
浏览 8
提问于2022-09-19
得票数 0
回答已采纳
1
回答
PCP和停机问题的时间和空间复杂性
complexity-theory
、
theory
、
number-theory
因此,PCP是半可
判定
的和不可
判定
的,停顿问题也是不可
判定
的。有没有可能为它们命名
一个
时间复杂度,比如NP或expTime? 那么空间复杂性呢:它们是在Pspace
中
吗?
浏览 12
提问于2020-02-23
得票数 0
回答已采纳
1
回答
SMT-LIB
中
的QF_NRA逻辑是可
判定
的吗?
z3
、
smt
、
theorem-proving
、
cvc4
SMT-LIB
中
的QF_NRA逻辑是可
判定
的吗? 我知道Tarski证明了非线性算法是可
判定
的,在实数
中
多项式系统是可
判定
的。然而,QF_NRA是否属于这一保护伞并不明显,因为QF_NRA包含除法。第
一个
问题是,QF_NRA
中
的除法是否包括分母可能为零的变量除法。,因为答案本身就足够困难了。如果零除法不是QF_NRA的一部分,那么QF_NRA
中
的除法就可以转换为乘法,这个问题将如Tarski所证明的那样是可
判定
的。如果QF_NRA<e
浏览 2
提问于2016-10-21
得票数 2
回答已采纳
1
回答
Z3:非线性整数算术不可
判定
还是半可
判定
?
z3
、
z3py
、
theorem-proving
、
first-order-logic
、
decidable
关键是这个结果完全让我大吃一惊,因为它返回了
一个
结果!这是令人惊讶的,因为我一直在研究一阶理论,据我所知,LIA是可
判定
的,而NIA则不是(在理性主义
中
也是如此)。结果是[],顺便说一句:有效。所以我在这一边搜索了这个问题,发现(),是莱昂纳多·德莫拉自己回答如下:如果
一个
公式有
一个
解,我们总是可以用蛮力找到它。也就是说,我们一直在列举所有可能的作业,并测试它们是否满足这个公式。在()
中
:G del证明了(NIA)是
一个
不可
判定
的问题。 另外,在()<
浏览 8
提问于2021-11-24
得票数 2
回答已采纳
3
回答
为什么递归枚举语言不能确定
computer-science
、
turing-machines
、
formal-languages
这是维基百科
中
可
判定
的定义。 递归集是可递归枚举集的子集。有一些递归枚举语言在递归集之外。那么,为什么递归枚举语言不能确定呢?
浏览 3
提问于2012-02-26
得票数 5
回答已采纳
1
回答
克莱恩星无法分辨
computer-science
、
complexity-theory
、
computation-theory
、
turing-machines
我知道,如果L是可
判定
的,我们可以通过构造
一个
图灵机来证明L*也是可
判定
的,但是我很难解决这个问题:如果L是不可
判定
的,那么L*也是不可
判定
的。这句话是真的还是假的?
浏览 2
提问于2017-10-03
得票数 1
1
回答
(半可
判定
)一阶理论的组合在Z3
中
是可能的,但实际的语义/签名组合又如何呢?
z3
、
smt
、
z3py
、
theorem-proving
、
first-order-logic
免责声明:这是
一个
相当理论性的问题,但认为它适合这里;如果不是,请告诉我另
一个
选择:)最近,我意识到可以在Z3
中
指定这种类型的公式:因此,为了理解这一点,我向自己提出了
一个
更简单的练习:以具有特定公式和签名集的可
判定</e
浏览 6
提问于2022-09-27
得票数 0
回答已采纳
1
回答
在少于n^2的情况下,Agda
中
的可
判定
等式?
functional-programming
、
metaprogramming
、
agda
、
dependent-type
、
theorem-proving
我有
一个
编程语言的AST的数据类型,我想解释一下,但AST大约有10个不同的构造函数。SeqTerm : Term -> Term -> Term人们如何在实践
中
浏览 0
提问于2017-07-18
得票数 2
1
回答
经典公理暗示每
一个
命题都是可
判定
的?
coq
在精益手册“精益证明定理”
中
,我读到:“用经典公理,我们可以证明每
一个
命题都是可
判定
的”。我想要求澄清这一声明,我在问
一个
Coq论坛,因为这个问题同样适用于Coq,也适用于精益(但我觉得我更有可能在这里得到答案)。当阅读“每个命题都是可
判定
的”时,我理解我们可以定义
一个
函数(或者至少我们可以证明这样
一个
函数的存在): Definition decide (p:Prop) : Dec p.所以我的问题是:假设没有错误,并且“用经典公理,我们可以证明每
一个
浏览 0
提问于2020-04-20
得票数 3
回答已采纳
1
回答
如果函数应用程序是
一个
典型的类型化呢?
haskell
、
type-inference
假设Haskell的函数应用程序( "space“运算符)是在
一个
类型
中
而不是在语言中。,这会使类型推断无法
判定
吗?,我的直觉说,它是这样的,但是我对类型推理的理解仅限于简单的辛德雷-米尔纳。作为后续行动,如果它是不可
判定
的,它是否可以通过取缔某些病理事件来
判定
?
浏览 3
提问于2016-02-09
得票数 5
回答已采纳
3
回答
C#静态
数组
绑定检查
c#
、
arrays
、
static-analysis
、
indexoutofboundsexception
、
formal-verification
是否有用于C#的工具可以静态地(不执行代码)检测出绑定
数组
访问,即将抛出的
数组
访问。 谢谢。编辑:是的,我知道在general
中
,理论上是不可能这样做的(也就是说,它是不可
判定
的),但这并不意味着在某些情况下不可能这样做(事实上,正式验证的整个领域是为理论上不可能的事情生产实用工具)。
浏览 6
提问于2013-12-06
得票数 1
回答已采纳
3
回答
NP-hard与不可
判定
问题的关系
algorithm
、
np-hard
、
decidable
我对不可
判定
问题和NP困难问题之间的关系感到有点困惑。NP难题是否是不可
判定
问题的子集,或者它们是相同和相等的,还是它们不具有可比性?
浏览 8
提问于2012-05-08
得票数 16
回答已采纳
2
回答
证明包含向量的数据类型的可
判定
性
recursion
、
coq
用(笔和纸)数学来表达这一点的通常方法是,你有一组函数符号,F,还有
一个
函数函数。表达式是一棵树,其中每个节点都被标记为
一个
函数符号,其子节点的数量与其属性相同。在这个特殊的例子
中
,我还得到了一组原子变量,这些变量被显式地作为术语注入。 很清楚如何用Coq (我在底部有一段代码)将其写下来,但我想证明某种可
判定
性的结果。我已经证明了向量的可
判定
性(“如果我对A有可
判定
性,那么我就可以得到VectorDef.tAn上的可
判定
性”),但是我想不出如何对我的树类型做同样的工作
浏览 0
提问于2019-03-25
得票数 2
回答已采纳
1
回答
证明这种语言是不可分辨的。
turing-machines
、
formal-languages
L= {M \M是图灵机描述,并且存在
一个
长度为k的输入x,使得M最多在k步之后停止。 我想是的,但我无法证明。我试着想办法从停下来的问题上减少一点。
浏览 1
提问于2011-07-10
得票数 6
回答已采纳
1
回答
为什么我们选择熵增益作为决策树学习的标准,而不是减少错误率作为标准?
machine-learning
、
artificial-intelligence
、
decision-tree
我一直在跟踪,在决策树( DT )学习
中
,选择熵增益作为选择
一个
特征/参数x_i作为DT自顶向下增长
中
另
一个
特征的子特征的
判定
标准。我们选择DT的目的始终是通过最小化错误率来避免过度拟合的;,那么我们为什么不使用错误率作为树自顶向下生长
中
的特征/参数选择的
判定
标准。
浏览 2
提问于2017-07-31
得票数 0
1
回答
图灵机不能接受的已知语言有哪些?
theory
、
turing-machines
、
computability
对于,不接受自己编码的图灵机的语言不能被任何图灵机接受。
浏览 36
提问于2012-06-27
得票数 9
回答已采纳
1
回答
Np完备性--在归约
中
需要一些澄清
algorithm
、
np-complete
、
np
、
np-hard
我想要对
一个
概念进行一些澄清。为了证明
一个
问题是NP完全的,我们使用约简。请给我
一个
澄清,并指导我解决上述问题。谢谢
浏览 8
提问于2012-11-19
得票数 0
1
回答
关于Coq
中
其他未知参数化命题的参数化
polymorphism
、
coq
、
decidable
、
parameterized-types
我想定义
一个
参数化命题decidable,它讨论其他参数化命题的可
判定
性。作为
一个
常见的例子,even是
一个
参数化命题,它采用nat类型的
一个
参数,并且是可
判定
的。lt是
一个
参数化命题,它采用nat型的两个参数,并且它也是可
判定
的。我希望decidable是这样的,decidable even和decidable lt都是可证明的命题。我认为在d_0
中
使用d_0作为
一个
前提应该是可以的,因为Coq将足够聪明地计算出P
浏览 2
提问于2014-08-22
得票数 0
回答已采纳
1
回答
Django序列化程序字段可选
python
、
django
、
serialization
、
checkbox
现在,我有
一个
输入和两个复选框,它们将把
一个
变量返回给python后端。我希望这两个复选框的默认值为false,如果选中它们,则返回true。我想我的问题是,当我使用序列化程序时,如果两个复选框未选中,我无法从这两个复选框
中
获得值。如果复选框被选中,我的代码将正常工作,并且该值将保存在模型
中
。如果不是,我会得到
一个
错误<input type="text" ng-model="var.name"> <input ng-model=&quo
浏览 1
提问于2017-08-12
得票数 0
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
js中数组的常用操作
js中Array.prototype.find 方法在对象数组上无效果,捉急……
从一个数组中移除重复对象
PHP数组获取最后一个元素,10个方式中哪个有错?
Node.js cluster 中监听同一个端口为什么不会报错
热门
标签
更多标签
云服务器
ICP备案
实时音视频
对象存储
即时通信 IM
活动推荐
运营活动
广告
关闭
领券