问题标签 [theorem-proving]

我的 Coq 证明有问题，希望得到一些帮助和指导。我的部分定义如下：

我想说“组件术语必须是连接的客户端或服务器；但不能同时是两者。” 我在 Coq 中提出了以下内容作为上述内容的表示（基于我上面的定义）：

但是，我不确定这是否正确（是吗？），因为当我得到证明时，我陷入了困境

的类型HotelRes确实是组件（在这种情况下，HotelRes是连接的客户端），但是，由于这不在假设集中，我不能使用确切或自动策略之类的东西。

我怎么能继续这样的证明？

有没有人尝试用 Z3 本身来证明Z3 ？

甚至有可能使用 Z3 来证明 Z3 是正确的吗？

更理论上，是否有可能证明工具 X 是正确的，使用 X 本身？

我正在寻找用 GNU Prolog 编写的重言式检查器的开源实现（也可以接受 SWI-Prolog 的实现，但首选 GNU Prolog）。

我想为程序输入提供如下查询：

或者

当然，符号可以不同，如下所示：

我期望的结果是布尔答案，例如“是/否”、“等于/不同”、“找到证明/未能找到证明”或类似的。

我在ftp://ftp.cs.yorku.ca/pub/peter/SVT/GNU/上找到了 GNU-Prolog 的重言式检查器，但没有附加许可证，也不知道如何应用Gnu Prolog 算术约束和算术功能为了用算术扩展逻辑模型。

• 还有其他类似的求解器吗？
• 一些示例如何使用算术能力来扩展模型。

谢谢，格雷格。

PS 根据算术，我正在寻找部分支持 - 我只想处理一些基本情况，如果提出的解决方案能够正确处理经典逻辑并打开，我可以使用简单的启发式手动编码（也欢迎 gnu-prolog 整数函数示例） -源代码会很好扩展:)。

PPS 正如@larsmans 所指出的，根据哥德尔的不完备性定理，没有办法证明“所有”公式。这就是为什么我正在寻找可以证明的东西，可以从给定的公理和规则集证明什么，因为我正在寻找 Gnu Prolog 程序，我正在寻找此类公理和规则集的示例；）。当然检查器可能会失败 - 我期待它会在“某些”情况下工作:)。- 另一方面，有哥德尔的完备性定理；）。

我正在使用 Z3 的 QBVF 求解器，想知道是否可以从存在断言中提取值。也就是说，假设我有以下内容：

这基本上说有一个“最少”的 16 位无符号值。那么，我可以说：

Z3-3.0 愉快地回应：

这真的很酷。但我想做的是能够通过 get-value 提取该模型的各个部分。不出所料，以下似乎都不起作用

在每种情况下，Z3 都正确地抱怨没有这样的常数。(check-sat)显然，Z3 拥有该信息，正如对呼叫的响应所证明的那样。有没有办法通过get-value或其他机制自动访问存在值？

谢谢..

I'm working through the ListSet module from the Coq standard library. I'm unsure how to reason about conditionals in a proof. For instance, I am having trouble with the following proof. Definitions are provided for context.

The current proof state includes the inr of Aeq_dec as a hypothesis. I have discarded the base case of induction and the inductive case where the inl of Aeq_dec is true.

The only way for H to be true if a <> x is if set_mem xs is true. I should be able to apply the conditional in H to a <> x in order to obtain set_mem xs. However, I don't understand how to do this. How do I deal with, or decompose, or apply conditionals?

How can we use Breadth First Search as a strategy for propositional theorem proving (I can't see a clear problem formulation: what are the actions available at each state and what a state is).

I've been looking for explanations everywhere in the net; all documents mention BFS but none of them gives an algorithm.

Thank you for your help

模式匹配（如在 Prolog、ML 系列语言和各种专家系统外壳中发现的）通常通过以严格的顺序逐个元素地匹配查询与数据来进行操作。

然而，在诸如自动定理证明之类的领域中，需要考虑一些运算符是关联的和可交换的。假设我们有数据

并查询

按照表面语法，这不匹配，但从逻辑上讲，它应该与$Xbound to匹配，A or B因为or它具有关联性和可交换性。

有没有任何语言的现有系统可以做这种事情？

我已经看过很多关于 SATCHMO 定理证明器的论文，它们讨论了 Prolog 的实现。但是到目前为止，我发现的唯一源代码实现在一本书中，它确实很有限，仅用于举例说明如何评估和触发规则。有人在 Prolog 中看到 SATCHMO 的良好开源实现吗？

请注意，我指的不是 Django 的 Python 语言工具 Satchmo，这就是为什么我没有在标签中包含 Satchmo，因为这是 Stack Overflow 显示为该标签的主要定义的原因。

我正在努力学习agda。但是，我遇到了一个问题。我在 agda wiki 上找到的所有教程对我来说都太复杂了，并且涵盖了编程的不同方面。在并行阅读了 3 篇关于 agda 的教程后，我能够编写简单的证明，但我仍然没有足够的知识来使用它来实现真实单词算法的正确性。

你能推荐我关于这个主题的任何教程吗？类似于 Learn Yourself a Haskell 但适用于 Agda 的东西。

当我编写算法时，我通常会在注释中写下不变量。

例如，一个函数可能返回一个有序列表，而另一个函数期望一个列表是有序的。
我知道定理证明存在，但我没有使用它们的经验。

我也相信智能编译器 [原文如此！] 可以利用它们来优化程序。
那么，是否可以写下不变量并让编译器检查它们？