自動定理證明

我正在尋找一個自動定理證明系統，它可以證明這一點：自動定理證明

鱷魚帶芒人的孩子。男人讓鱷魚不要吃他的孩子。但鱷魚說：如果你會告訴我，我會把你的孩子交還給你，我將如何處理他。

解析解他看起來像這樣：

X - 鱷魚會吃小孩 Ÿ - 男人的答案：鱷魚會吃小孩

〜意味着平等，！指的不是， - >暗示，+ OR;

((x~y)->!x) and ((x XOR y)->x) = 
(x! and y +!x and y+!x)(!x!y+x and y+x) = 
(!x+!y)(x+!y) = !y;

因此，答案是，男人不得不說：「你不會吃孩子」;

現在，有很多在這裏列出系統： http://en.wikipedia.org/wiki/Automated_theorem_proving

我已經試過的5-6，但不能真正理解我在做什麼在這裏。如何來規範這個定理在他們裏面，這樣我就可以進入它的第一部分：

((x~y)->!x) and ((x XOR y)->x)

，並得到答案

y作爲輸出。

任何一次的建議，哪個系統至少可以自動完成，並給我更多的提示？

Regards， Konstantin。

來源

2013-06-25 user2426290

經過大量的研究，我發現有很多這樣的程序，所以我的答案是：是的，這樣的定理可以自動證明。在線示例：http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-zentral.html

來源

2013-07-13 12:59:53 user2426290

你能分享一下鱷魚問題的代碼嗎？ –

結帳序言。對於邏輯命題和類似的事情來說，這很好。從閱讀維基開始，看看它聽起來像你想要的。它是一種邏輯編程語言 - 它會幫助你建立自己的定理證明算法。

百科： http://en.wikipedia.org/wiki/Prolog

教程： http://cs.union.edu/~striegnk/courses/esslli04prolog/index.php

來源

2013-06-25 14:31:54 RutledgePaulV

感謝您的回答。我試圖用prolog解決這個問題，但是失敗了。實際上，我可以爲這個特定任務編寫求解器，但是我想要解決許多類比問題的解決方案，而且我自己也做不到。例如，在Prolog中，我需要編寫雙重子句形式來表示任何公式，僅作爲連接詞和否定詞，而e.t.c，還有其他許多要考慮的事項，這不是非常簡單的任務。那就是我想從現成的開源解決方案中選擇一些東西並開始研究它們。但我可以'找到任何可以解決我提供的配方 – user2426290

嗯，你的問題的目標，它比平常高很多，我不夠了解你的任務就是要幫助......

我只是在Prolog中隱藏了'tableaux'，並且會建議在深入研究something more sophisticated之前先嚐試simpler one（但我甚至不知道這種邏輯是否適合您的任務）。

來源

2013-06-25 17:36:10 CapelliC

謝謝，這實際上是一個好的開始。我還創建了PROLOG的SATCHMO源代碼，也會試用它。我的問題是，我不知道 - 如果這個公式真的可以自動作爲一般原因被解決，但我認爲是這樣，所以我希望有人可以批准這一點，並指出我正確的方向。但無論如何，我不會浪費我的時間，同時會嘗試使用PROLOG自己來實現它。實際的求解算法並不是很難：基於一些規則，每一步都簡化了公式（比如，我們可以用x和y代替x->直到我們有連詞和否定 – user2426290

http：//en.wikipedia。 org/wiki/Method_of_analytic_tableaux - 實際上也許這正是我需要的，從維基百科我可以看到它非常接近。我現在試試這個方法 – user2426290

自動定理證明

回答

相關問題