时间戳

首页 > 解决方案 > Prover9 "Some, but not all, of the requested proofs were found"

logic - Prover9 "Some, but not all, of the requested proofs were found"

问题描述

I'm running some lattice proofs through Prover9/Mace4. Prover9's saying Exit: Time limit. plus the message in the Title.

I've doubled the time limit from 60 to 120 seconds. Same message (in twice the time). The weird thing is:

I've found some GHits for that message, but they seem to be all in Chinese(?)

It's possible the axioms I've given are (mutually) recursive -- I'm trying to introduce a function and a nominated 'absorbing element' [**]; and that solving will need infinitary unification. Does Prover9 do that?

I'm happy to add the axioms and goal to this message. (I'm using a non-standard way to define the meet and join.) But first, are there any sanity checks I should go through?

[**] the absorbing element is neither lattice top nor lattice bottom; more like lattice left-corner. (The element will be lattice bottom just in case the lattice degenerates to two elements.) The function is a partial ordering 'at right angles' to top/bottom. The lattice I expect to be neither complemented nor distributive (again except when 2 elements).

标签： logictheorem-proving

解决方案

经过多次尝试，我已经重现了这一点，但只是通过设置一些我确信我不会触及的奇怪选项。（我通常更改的唯一选项是Time limit，而且我Reset to defaults经常更改，所以这会掩盖任何证据。）

这是我对发生的事情的猜测。

怎么了but not all？

  • 您可以输入多个目标（前提是它们都是积极的）。[**]

  • 奇怪的选项设置，如果 Prover9 可以证明第一个但不能证明第二个，它会一直尝试直到用尽；但随后只报告成功的——$F.结果OK。

  • 如果你把时间限制加倍，它仍然会证明第一个并且仍然继续尝试第二个——花费两倍的时间来获得相同的结果。

  • Mace4 将遇到第一个目标，并花时间尝试反例。没有一个，因为它是可证明的。同样，将其时间限制加倍将在加倍后得到相同的结果。

[注意**] 我从来没有打算设定多个目标；但是当我使用公理进行黑客攻击/实验时，我将所有目标都保留在Goals:框中，以便我可以轻松地切换取消/评论。我想我在取消注释另一个时没有注释掉一个。

如手册中所述，行为通常是 Prover9 在它证明的第一个目标上报告成功；不会继续其他目标。如果有多个可证明的目标，它似乎选择最简单/最快的（？），而不考虑文件中的位置。

但是max_proofs设置为超过默认值 1时，Prover9 将继续尝试。（还有一个auto_denials标志与它有关，我不明白。）

我不知道我是如何设置的——当我最终找到子屏幕时，我max_proofs没有认出它。Options/Limits诡异的。

推荐阅读