軟件解決一個邏輯難題

Question

Here我發現了一個迷人的，如果很容易的邏輯問題：

在該名單中的回答是正確答案這個問題？

1. 以下全部。
2. 以下都不是。
3. 以上全部。
4. 其中之一。
5. 以上都不是。
6. 以上都不是。

這將是很容易重新編寫這些命題在一些編程語言語句：

def p1 = p2 && p3 && p4 && p5 && p6 
def p2 = !p3 && !p4 && !p5 && !p6 
def p3 = p1 && p2 

等。更難的是真正運行這樣的程序，而不會陷入無限循環。

有沒有一種語言或圖書館（或其他東西）可以或多或少地解決這個問題？我在想Prolog，因爲我對Prolog的所有了解都是用來解決「這樣的問題」。

代碼是什麼樣的？

Answer 1

用Prolog來解決這樣的邏輯謎題確實微不足道。

例如，一種方法是使用CLP（B），它代表約束邏輯 編程過布爾變量並有自己的 標籤，clpb。

幾個Prolog系統附帶CLP（B）求解器。 SICStus Prolog就是一個非常突出的例子。

這種方法的核心思想是將布爾 變量上的約束滿足問題表示爲  （CSP）。

在這個具體的例子，例如，我們可以使用命題 變量一個，A ，...，A 來表示不同的方法來回答這個問題。每個答案都將這些變量之一與其他幾個 相關聯，反映了答案對其他答案的說明。

使用SICStus Prolog的，什麼每個答案的手段可能看起來像 這樣的聲明描述：

 
:- use_module(library(clpb)). 

solution([A1,A2,A3,A4,A5,A6]) :- 
     sat(A1 =:= A2*A3*A4*A5*A6), 
     sat(A2 =:= ~(A2+A3+A4+A5+A6)), 
     sat(A3 =:= A1*A2), 
     sat(A4 =:= card([1],[A1,A2,A3])), 
     sat(A5 =:= ~(A1+A2+A3+A4)), 
     sat(A6 =:= ~(A1+A2+A3+A4+A5)). 

從下面的查詢，我們看到只有一個答案在邏輯上是可以受理受這些 約束：

 
?- solution(Vs). 
Vs = [0, 0, 0, 0, 1, 0]. 

因此，答案是唯一可以保持所有陳述 一致的選項。

一種無限循環不能在這樣的製劑出現，由於各個約束的每個總是終止，而且整個程序僅由這樣的約束的序列組成。

的約束求解器具有自動推導出的單一允許解，使用被稱爲約束  傳播過程。