% CM30071 COURSEWORK
% University of Bath
% Alessio Guglielmi 5/3/07
%
% Topic 4
%
% We want to show that first order logic is undecidable by using the known fact
% that the Post Correspondence Problem (PCP) is undecidable.
%
% Please see in the next page a definition and example of PCP, and consider a
% given the fact that the problem is undecidable.
%
% Below, you find a Prolog program which solves the PCP and which is also a
% theory in first order logic. If first order logic was decidable, PCP would be
% decidable, too, which is absurd.
% Encoding of PCP: 1 - the two sets of words (this corresponds to the example
% given in the following page):
string_W( s(0),Y, g(Y)).
string_W(s(s(0)) ,Y,g(f(g(g(g(Y)))))).
string_W(s(s(s(0))),Y, g(f(Y))).
string_X( s(0),Y,g(g(g(Y)))).
string_X( s(s(0)),Y, g(f(Y))).
string_X(s(s(s(0))),Y, f(Y)).
% Encoding of PCP: 2 - definition of the problem:
pcp_init(W,X) :- string_W(I,0,W),
string_X(I,0,X).
pcp_aux(W,X) :- pcp_init(W,X).
pcp_aux(W,X) :- pcp_aux(W1,X1),
string_W(I,W1,W),
string_X(I,X1,X).
pcp(S) :- pcp_aux(S,S).
% Encoding of PCP: 3 - the goal:
:- pcp(S).
% This defines the PCP in pure Prolog, which corresponds also to a first order
% predicate logic theory.