问题标签 [theorem-proving]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
coq - 在 Coq 中用假假设完成证明
所以我在子目标中有一个错误的假设。这是不同构造函数之间的相等性。如何完成子目标?
z3 - Z3和coq的区别
我想知道是否有人可以告诉我Z3和coq之间的区别?在我看来,coq 是一个证明助手,因为它要求用户填写证明步骤,而 Z3 没有这个要求。但似乎 coq 也有类似于 Z3 的自动战术?又或者 coq 的证明搜索能力没有 Z3 强大?
verification - Limits of SMT solvers
Traditionally most work with computational logic was either propositional, in which case you used a SAT (boolean satisfiability) solver, or first-order, in which case you used a first-order theorem prover.
In recent years, a lot of progress has been made on SMT (satisfiability modulo theory) solvers, which basically augment propositional logic with theories of arithmetic etc.; John Rushby of SRI International goes so far as to call them a disruptive technology.
What are the most important practical examples of problems that can be handled in first-order logic but still can't be handled by SMT? Most particularly, what sort of problems arise that can't be handled by SMT in the domain of software verification?
java - Java 中的 BDD 实现
有人对 Java 中的 BDD(二进制决策图)实现(或提供 Java 绑定的实现)有建议吗?我在网上找到了这个页面:http: //www.mancoosi.org/~abate/avalaible-bdd-libraries但不确定它是否已过时。还是只使用 Prolog 实现有意义?
coq - 在 Coq 中使用存在定理
我在 Coq 中有以下定理:Theorem T : exists x:A, P x.
我希望能够在后续证明中使用这个值。IE 我想说这样的话:“让o
代表一个这样的值P o
。我知道它o
是由定理存在的T
......”
我该怎么做?提前致谢!
artificial-intelligence - 用 A* 算法证明定理
我正在准备硕士学位的期末考试,这是过去考试的问题,我真的很困惑,不知道从哪里开始。
我的想法是可接受的启发式是解析规则,然后证明解析规则是可接受的,对吗?如果是这样,要证明解决规则是可以接受的,我应该从哪里开始?感谢您的帮助。
考虑一个定理证明器的应用。A* 算法可用于搜索最简单(最短)的证明。假设已知公理和定理在命题逻辑中表示为霍恩子句的知识库,并且证明者使用反向链接。
(a) 提出一个可接受的启发式。
(b) 证明提议的启发式是可以接受的
probability - 从 Z3 中的一组令人满意的任务中统一采样
有没有办法使用 Z3 定理证明器从一组令人满意的作业中均匀采样?如果不是,那么最接近 Z3 且具有此功能的系统是什么?
coq - 解决这个 coq 练习
我正在学习 COQ,但我被困在书中的一个练习中。这本书没有给我一个解决方案,所以我不知道该怎么做。虽然我已经完成了第一个。我必须将这些语句转换为谓词逻辑:
代码:
.
你能帮忙吗?非常感谢!
coq - Coq:根据唯一性和存在性定理定义函数
为了尽可能地隔离这个问题,假设我开始一个 Coq 会话,如下所示。
从这里开始,我想将一个函数定义为始终为真的f : A -> B
唯一函数。P a (f a)
我怎样才能做到这一点?我可以这样做吗?显然我应该从类似的东西开始
...但是我如何根据这些假设实际编写函数?
coq - 迷失在这个练习中
我必须证明这一点:
到目前为止,我已经完成了:
然后我必须证明 False。我不知道该怎么做。这是不可证明的吗?你能把我引向正确的方向吗?或者我在这里错过了什么?
编辑:Ptival,你帮了大忙……我注意到问题上有一个错误,当我尝试编辑问题时,我不小心点击了删除按钮,惊慌失措并按下退格键。:(