将一阶逻辑转换为 Prolog

Question

我需要将以下 FOL 句子表述为 Prolog 规则，并且完全不知道如何做到这一点。 （我是 Prolog 的新手）：

“如果两个终端相连，则它们具有相同的信号。” 在一阶逻辑中，这将是：

FORALL(T1, T2) : Terminal(T1) AND Terminal(T2) AND Connected(T1, T2) => Signal(T1) = Signal(T2)

我知道，“and”是如何用 Prolog 编写的，而且你不需要 FORALL。我的问题是，左侧只能是一个谓词。 这是一个更大问题的一部分，完整的规则集是：

1. 如果两个端子相连，则它们具有相同的信号
2. 连通是可交换的
3. 每个终端的信号不是1就是0
4. 有四种类型的门（and、or、xor、neg）
5. 与门的输出为 0 当且仅当其任何输入为 0 时
6. 当且仅当其任何输入为 1 时，或门的输出为 1
7. 当且仅当输入不同时，异或门的输出为 1
8. 否定门的输出与输入不同
9. 门（除了 neg）有两个输入和一个输出
10. 电路的输入和输出数量达到其极限，并且没有超出其数量的端子
11. 门、终端、信号、门类​​型和任何东西都是不同的
12. 门是电路

我目前正在制定规则，我会在完成后立即发布。这是我到目前为止所拥有的（第一行 % 是自然语言，第二行 % 是直观的 FOL 表示，之后的行是我对 Prolog 规则的尝试）：

%If two terminals are connected, then they have the same signal:
%all(T1, T2) : terminal(T1), terminal(T2), connected(T1, T2) => signal(T1) = signal(T2).
same_value(T1, T2) :- terminal(T1), terminal(T2), connected(T1, T2).

%Connected is commutative:
%all(T1, T2) :- connected(T1, T2) <=> connected(T2, T1).
connected(T1, T2) :- connected(T2, T1).

%The signal at every terminal is either 1 or 0:
%all(T) :- terminal(T) => signal(T) == 1; signal(T) == 0.
terminal(T) :- signal(T) = 1; signal(T) = 0.

%There are four types of gates:
%all(G) :- (gate(G), K = type(G)) => (K == and; K == or; K == xor; K == neg).

%An and gate's output is 0 if and only if any of its inputs is 0:
%all(G) :- gate(G), type(G) == and => signal(out(1, G)) = 0 <=> some(N), signal(in(N, G)) == 0.
signal(out(1, G)) :- (gate(G), type(G) == or, signal(in(1, G)) == 0; signal(in(2, G)) == 0) => 0.
signal(out(1, G)) :- (gate(G), type(G) == or, signal(in(1, G)) == 1, signal(in(2, G)) == 1) => 1.
%this produces an error: Operator expected

%An or gate's output is 1 if and only if any of its inputs is 1:
%all(G) :- gate(G), type(G) == or => signal(out(1, G)) = 1 <=> some(N), signal(in(N, G)) == 1.
signal(out(1, G)) :- (gate(G), type(G) == or, signal(in(1, G)) == 0, signal(in(2, G)) == 0) => 0.
signal(out(1, G)) :- (gate(G), type(G) == or, signal(in(1, G)) == 1; signal(in(2, G)) == 1) => 1.
%this produces an error: Operator expected

%An xor gate's output is 1 if and only if its inputs are different:
%all(G) :- gate(G), type(G) == xor => signal(out(1, G)) = 1 <=> signal(in(1, G)) \= signal(in(2, G)).
signal(out(1, G)) :- (gate(G), type(G) == xor, signal(in(1, G)) == signal(in(2, G))) => 0.
signal(out(1, G)) :- (gate(G), type(G) == xor, signal(in(1, G)) \= signal(in(2, G))) => 1.
%this produces an error: Operator expected

%A neg gate's output is different from its input:
%all(G) :- gate(G), type(G) == neg => signal(out(1, G)) = not(signal(in(1, G))).
signal(out(1, G)) :- (gate(G), type(G) == neg, signal(in(1, G)) == 1) => 0.
signal(out(1, G)) :- (gate(G), type(G) == neg, signal(in(1, G)) == 0) => 1.
%this produces an error: Operator expected

%The gates (except for neg) have two inputs and one output:
%all(G) :- gate(G), type(G) == neg => arity(G, 1, 1).
%all(G) :- gate(G), K = type(G), (K == and; K == or; K == xor) => arity(G, 2, 1).
arity(G, 1, 1) :- gate(G), type(G) == neg.
arity(G, 2, 1) :- gate(G), (type(G) == and; type(G) == or; type(G) == xor).

%A circuit has terminals up to its input and output arity, and nothing beyond its arity:
%all(C, I, J) :- circuit(C), arity(C, I, J) =>
%   all(N), (N =< I => terminal(in(C, N))), (N > I => in(C, N) = nothing),
%   all(N), (N =< J => terminal(out(C, N))), (N > J => out(C, N) = nothing).

%Gates, terminals, signals, gate types, and Nothing are all distinct:
%all(G, T) :- gate(G), terminal(T) => G \= T \= 1 \= 0 \= or \= and \= xor \= neg \= nothing.

%Gates are circuits:
%all(G) :- gate(G) => circuit(G).
circuit(G) :- gate(G).

Answer 1

答案并不简单。第一种可能性：

相同信号（T1，T2）：- 终端（T1），终端（T2）， 已连接（T1，T2）。

一个更复杂的，假设term(T,S)的意思是'终端T有信号S'

checkSignals(term(T1,S1), term(T2,S2)) :- 终端(T1), 终端(T2), 已连接（T1，T2），S1=S2。

或简单地使用相同的变量：

checkSignals（术语（T1，S），术语（T2，S））：-终端（T1），终端（T2）， 已连接（T1，T2）。

如果这是更普遍问题的一部分，请展示整个问题以寻找更好的解决方案。