Convert first order logic into Prolog

Question

I need to formulate the following FOL sentence as Prolog rule and have absolutely no clue how to do that. (I am new to Prolog):

"If two terminals are connected, then they have the same signal." In first order logic this would be:

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

I do know, how "and" is written in Prolog and also that you do not need a FORALL. My problem ist, that the left side can only be one predicate. This is part of a larger problem, the complete rule set would be:

If two terminals are connected, then they have the same signal
Connected is commutative
The signal at every terminal is either 1 or 0
There are four types of gates (and, or, xor, neg)
An and gate's output is 0 if and only if any of its inputs is 0
An or gate's output is 1 if and only if any of its inputs is 1
An xor gate's output is 1 if and only if its inputs are different
A neg gate's output is different from its input
The gates (except for neg) have two inputs and one output
A circuit has terminals up to its input and output arity, and Nothing beyond its arity
Gates, terminals, signals, gate types, and Nothing are all distinct
Gates are circuits

I am currently trying to formulate the rules, I will post them as soon as I am finished. This is what I have so far (first line with % is natural language, second line with % is an intuitive FOL representation, lines thereafter are my attempt of a Prolog rule):

%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).

Have you familiarized yourself with Prolog at all via tutorial or book? FYI, the first expression, If two terminals are connected, then they have the same signal is quite directly and trivially translatable into a Prolog predicate. You don't need the FORALL. The AND is very basic: it's a comma. — lurker
@lurker: that's not completely true, In Prolog, one defines an order. Answer Set Programming is in many cases better to specify (real) logic. — Willem Van Onsem
@CommuSoft, I agree, not always true. I was saying for the OP's expressed case, not having any additional info, it's a simple predicate. — lurker

RafaelCaballero RafaelCaballero · Accepted Answer · 2015-02-18T18:44:34

The answer is not straightforward. A first possibility:


    sameSignal(T1,T2) :- terminal(T1),terminal(T2),
                         connected(T1,T2).

A more complicated, assuming that term(T,S) means 'the terminal T has signal S'


    checkSignals(term(T1,S1), term(T2,S2)) :- terminal(T1), terminal(T2), 
                                              connected(T1,T2), S1=S2.

or simply using the same variable:


    checkSignals(term(T1,S), term(T2,S)) :- terminal(T1), terminal(T2),
                                            connected(T1,T2).

If this is part of a more general problem please show the whole problem to look for a better solution.

Convert first order logic into Prolog

1 Answers