作者keroro97 (keroro)
看板logic
标题[请益] prover9
时间Thu Jan 28 10:53:22 2010
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.
请问怎麽会这样 谢谢~
以下是详细资讯；
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.01) seconds.
% Length of proof is 5.
% Level of proof is 2.
% Maximum clause weight is 0.
% Given clauses 0.
1 (exists x exists y (x != y & G(x) & G(y))) # label(non_clause).
[assumption].
2 (exists x G(x)) # label(non_clause) # label(goal). [goal].
3 -G(x). [deny(2)].
4 G(c1). [clausify(1)].
7 $F. [resolve(3,a,4,a)].
============================== end of proof ==========================
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 118.169.224.47
1F：→ Searle:这要去程式版(? 01/28 18:19