问题标签 [theorem-proving]

我正在尝试使用 Kowalski 图算法进行分辨率定理证明。http://www.doc.ic.ac.uk/~rak/对算法的描述 没有说明如何处理它生成的大量重复子句。我想知道是否有一种众所周知的技术来处理它们？

特别是，您不能简单地抑制重复子句的生成，因为它们附带的链接是相关的。

在我看来，可能有必要跟踪迄今为止生成的所有子句的集合，并且当生成重复项时，将新链接添加到现有实例。即使在名义上删除子句时，这也可能需要维护，因为当它重新生成时。

重复可能需要根据文本表示来定义，而不是对象相等，因为不同子句的文字即使它们相同也是不同的对象。

谁能确认我在这里是否走在正确的轨道上？另外，我能找到的关于这个算法的唯一重要的在线参考是上面的链接，有没有人知道其他的，或者任何现有的实现它的代码？

I have a set of A's and a set of B's, each with an associated numerical priority, where each A may match some or all B's and vice versa, and my main loop basically consists of:

Take the best A and B in priority order, and do stuff with A and B.

The most obvious way to do this is with a single priority queue of (A,B) pairs, but if there are 100,000 A's and 100,000 B's then the set of O(N^2) pairs won't fit in memory (and disk is too slow).

Another possibility is for each A, loop through every B. However this means that global priority ordering is by A only, and I really need to take priority of both components into account.

(The application is theorem proving, where the above options are called the pair algorithm and the given clause algorithm respectively; the shortcomings of each are known, but I haven't found any reference to a good solution.)

Some kind of two layer priority queue would seem indicated, but it's not clear how to do this without using either O(N^2) memory or O(N^2) time in the worst case.

Is there a known method of doing this?

Clarification: each A must be processed with all corresponding B's, not just one.

我正在寻找一种工具（首选 GUI，但 CLI 可以），它允许我输入数学表达式，然后对它们执行操作，但将我限制为仅在数学上有效的操作。此外，该工具必须能够保存会话并稍后证明给定的一组已保存操作是有效的。

注意：我不是在寻找生成证明的系统，只是检查我手动指定的步骤是否有效。

我已经将ACL2用于类似的操作，并且在某些情况下效果很好，但在其他所有情况下都很难使用。

这个小项目是我的动力。它是一种 D 模板类型，允许求解方程。给定这个等式：

任何一个符号都可以设置为未知，并且评估该表达式将导致对该变量的赋值。它的工作原理是将表达式树构建到类型中，然后使用重写规则将其转换为可以为未知类型触发的东西。

我需要的是某种方法来验证重写规则。它们可以通过测试一个断言来验证，即给定一些关系是真的，另一个也是真的。

我正在用组合逻辑进行一些定理证明实验，这看起来很有希望，但有一个绊脚石：有人指出，在组合逻辑中，例如 I = SKK 是真的，但这不是一个定理，它必须作为公理添加。有谁知道需要添加的公理的完整列表？

编辑：您当然可以手动证明 I = SKK，但除非我遗漏了什么，否则它不是具有相等性的组合逻辑系统中的定理。话虽如此，您可以将 I 宏扩展为 SKK ......但我仍然缺少一些重要的东西。取一组子句 p(X) 和 ~p(X)，它们很容易解决普通一阶逻辑中的矛盾，并将它们转换为 SK，执行替换并评估 S 和 K 的所有调用，我的程序生成以下（我使用 ' 作为 Unlambda 的反引号）：

''eq '''s ''s 'ks ''s 'ks '' kk 'k eq ''s 'ks 'kk 'kk ''s 'kk 'k 假'k 真的'k 真的

看起来我可能需要一套适当的规则来处理部分调用'k和''，我只是没有看到这些规则应该是什么，我在这个领域能找到的所有文献都是为目标受众是数学家而不是程序员。我怀疑一旦你理解了答案，答案可能很简单。

我试图证明 ~(a->~b) => a 在希尔伯特风格系统中的陈述。不幸的是，似乎不可能想出一个通用的算法来找到一个证明，但我正在寻找一种蛮力类型的策略。欢迎任何关于如何攻击它的想法。

我试图在 Agda 中证明一个简单的引理，我认为这是正确的。

如果一个向量有两个以上的元素，则取其head后取与立即init取其相同head。

我将其制定如下：

这给了我；

作为回应。

我不完全了解如何阅读该(init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs))组件。我想我的问题是；是否可能，该术语的含义和含义。

非常感谢。

我听说过一些关于使用自动定理证明器试图证明软件系统中不存在安全漏洞的信息。一般来说，这很难做到。

我的问题是，有没有人使用类似的工具来查找现有或拟议系统中的漏洞？

Eidt：我不是要证明软件系统是安全的。我问的是寻找（最好是以前未知的）漏洞（甚至它们的类别）。我在想（但不是）这里的黑帽：描述系统的形式语义，描述我想要攻击的内容，然后让计算机找出我需要使用什么动作链来接管你的系统。

我在 Coq 中玩耍，试图创建一个排序列表。我只想要一个接受列表[1,2,3,2,4]并返回类似内容的函数Sorted [1,2,3,4]- 即取出坏部分，但实际上并未对整个列表进行排序。

我想我会先定义一个lesseqtype的函数(m n : nat) -> option (m <= n)，然后我可以很容易地对其进行模式匹配。也许这是个坏主意。

我现在遇到的问题的症结在于（片段，底部的整个功能）

不是类型检查；它说它期待一个option (m <= n)，但它Some (le_n 0)有 type option (0 <= 0)。我不明白，因为在这种情况下显然两者m和n都是零，但我不知道如何告诉 Coq。

整个功能是：

也许我正在超越自己，只需要在解决这个问题之前继续阅读。

我计划在 C 代码的符号执行方面进行一些实验，使用现成的 SMT 求解器，并想知道使用哪个求解器；例如，查看 SMT 竞赛的参赛者，仅采用开源系统，将其范围缩小到 Beaver、Boolector、CVC3、OpenSMT、Sateen、Sonolar、STP、Verit；这仍然是一个很长的清单。

试图进一步缩小范围，我注意到一些系统宣传处理位向量算术的能力，而其他系统只宣传处理一般整数算术的能力。原则上，前者对于 C 是正确的，其中变量是机器字，而不是无界整数。它在实践中有多大的不同？如果您尝试使用通用整数系统来完成此类工作，会发生什么情况？以下情况之一是否适用？

1. 位向量系统的效率稍高一些，但您可以使用其中任何一个，没问题。

2. 您可以使用稍作调整的通用整数系统。

3. 一般整数系统适用于有符号整数（因为溢出的结果未定义），但会给出无符号的错误答案。

4. 一般的整数系统对于机器字算术来说是不正确的，我可以将我的短名单减少到只有那些提供位向量算术的系统。

5. 还有什么……？

我试图尽可能具体地提出一个问题，但如果有人可以提出任何其他标准来缩小列表范围，那就太好了！

我试图在列表中搜索一个对象，然后如果找到它可能返回 true；否则为假。

但是，我试图想出的是不正确的。我真的很感激一些指导。我需要该函数通过将列表的头部与相关元素进行比较来搜索元素列表，如果不匹配，则递归地将列表的其余部分通过函数并重复，通过匹配列表的头部。

非常感谢您的指导和帮助。

先感谢您