作者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)