问题标签 [theorem-proving]

所以我在子目标中有一个错误的假设。这是不同构造函数之间的相等性。如何完成子目标？

我想知道是否有人可以告诉我Z3和coq之间的区别？在我看来，coq 是一个证明助手，因为它要求用户填写证明步骤，而 Z3 没有这个要求。但似乎 coq 也有类似于 Z3 的自动战术？又或者 coq 的证明搜索能力没有 Z3 强大？

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 中的 BDD（二进制决策图）实现（或提供 Java 绑定的实现）有建议吗？我在网上找到了这个页面：http: //www.mancoosi.org/~abate/avalaible-bdd-libraries但不确定它是否已过时。还是只使用 Prolog 实现有意义？

我在 Coq 中有以下定理：Theorem T : exists x:A, P x.我希望能够在后续证明中使用这个值。IE 我想说这样的话：“让o代表一个这样的值P o。我知道它o是由定理存在的T......”

我该怎么做？提前致谢！

我正在准备硕士学位的期末考试，这是过去考试的问题，我真的很困惑，不知道从哪里开始。

我的想法是可接受的启发式是解析规则，然后证明解析规则是可接受的，对吗？如果是这样，要证明解决规则是可以接受的，我应该从哪里开始？感谢您的帮助。

考虑一个定理证明器的应用。A* 算法可用于搜索最简单（最短）的证明。假设已知公理和定理在命题逻辑中表示为霍恩子句的知识库，并且证明者使用反向链接。

(a) 提出一个可接受的启发式。

(b) 证明提议的启发式是可以接受的

有没有办法使用 Z3 定理证明器从一组令人满意的作业中均匀采样？如果不是，那么最接近 Z3 且具有此功能的系统是什么？

我正在学习 COQ，但我被困在书中的一个练习中。这本书没有给我一个解决方案，所以我不知道该怎么做。虽然我已经完成了第一个。我必须将这些语句转换为谓词逻辑：

代码：

.

你能帮忙吗？非常感谢！

为了尽可能地隔离这个问题，假设我开始一个 Coq 会话，如下所示。

从这里开始，我想将一个函数定义为始终为真的f : A -> B唯一函数。P a (f a)

我怎样才能做到这一点？我可以这样做吗？显然我应该从类似的东西开始

...但是我如何根据这些假设实际编写函数？

我必须证明这一点：

到目前为止，我已经完成了：

然后我必须证明 False。我不知道该怎么做。这是不可证明的吗？你能把我引向正确的方向吗？或者我在这里错过了什么？

编辑：Ptival，你帮了大忙……我注意到问题上有一个错误，当我尝试编辑问题时，我不小心点击了删除按钮，惊慌失措并按下退格键。:(