作者yauhh (哟)
看板logic
标题Re: [请益] prover9
时间Thu Jan 28 20:01:40 2010
※ 引述《keroro97 (keroro)》之铭言：
: Assumption：
: exists x ( exists y ( x!=y & (G(x) & G(y)) )).
: Goals:
: exists x G(x).
: 却跑出 Prover9 Exit:Exhausted.
: Some, but not all, of the requested proofs were found.
在视窗环境把 Output 打开来看,里面把故事说得蛮清楚的.
在这个例子先把 -G(x), G(c1), G(c2) 化掉,但还剩一个 x != y 要找答案,
结果它真的找不到答案,所以回报 Exhausted.
我把你要问的换个写法:
Assumption:
exists x exists y (G(x)&G(y)).
all x all y (G(x)&G(y)->x!=y).
Goals:
exists x G(x).
证出来也是 False.
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 61.231.69.23
1F：推 keroro97:你的新写法和我原来的不等价 01/28 21:37
2F：→ keroro97:Assumption第二式Domain存在一个东西就炸掉了 01/28 21:39
3F：→ yauhh:嗯,对,x=y就有问题 01/28 21:47
查了一下Prover9论坛,有人恰好在十几天前有跟你一样的问题.
问题在程式处理步骤上,当它有东西没消化完,都会去找解. 找不到就回报搜寻失败.
http://forums.prover9.org/viewtopic.php?f=1&t=110
它说打个clear(auto_denials).指令就可以了满足那篇原po想要证出东西就完成的需求.
本篇我的作法没解决问题,只是想写出一些式子能绕过程式处理步骤而已.
※ 编辑: yauhh 来自: 61.231.69.23 (01/28 22:18)