% ----------------------------------------------------------------------
% Axiomatizations of finite-graph properties and their applications
% Chuck Liang, for CPSC 203, December 1998.

% Graphs are represented as lists of edges as in [(a,b), (b,c), (a,c)].

domain([1,2,3,4]).  % domain of the relation
graph1([(a,b), (a,c), (b,a), (c,a)]).  % a sample graph

reflexive(G) :- domain(Ns),  % domain can also be passed in as an arg.
	        nott( (inlist(N,Ns), nott(inlist((N,N), G))) ).

symmetric(G) :- nott( (inlist((X,Y),G), nott(inlist((Y,X),G))) ).


transitive(G) :- nott( (inlist((X,Y), G), inlist((Y,Z), G), 
	              nott(inlist((X,Z), G))) ).

antisymmetric(G) :- nott( (inlist((X,Y),G), inlist((Y,X),G), nott(X=Y)) ).

irreflexive(G) :- nott( inlist((X,X),G) ).

eqrelation(R) :- reflexive(R), symmetric(R), transitive(R).

% weak and strict (strong) partial orders:
wpo(R) :- reflexive(R), antisymmetric(R), transitive(R).
spo(R) :- irreflexive(R), antisymmetric(R), transitive(R).

r1([(1,2), (2,2)]).
r2([(1,2), (2,3), (1,3), (2,1)]).
r3([(1,1),(2,2),(2,3),(3,2),(3,3)]).
r4([(1,2),(2,3)]).



%  Closure operations:

% --- refclosure(G,RG) iff RG is the reflexive closure of G:
refclosure(G,G) :- reflexive(G).
refclosure(G,RG) :- domain(Ns), 
	            inlist(N,Ns), nott(inlist((N,N), G)),
		    refclosure([(N,N)|G],RG).

% --- symclosure(G,SG) iff SG is the symmetric closure of G:
symclosure(G,G) :- symmetric(G).    % G is already symmetric
symclosure(G,SG) :- inlist((X,Y), G), nott(inlist((Y,X), G)), 
	            symclosure([(Y,X)|G], SG).


% --- transclosure(G,TG) iff TG is the transitive closure of G:
transclosure(G,G) :- transitive(G).
transclosure(G,TG) :- inlist((X,Y), G), inlist((Y,Z), G), 
	              nott(inlist((X,Z), G)), 
		      transclosure([(X,Z)|G], TG).


% --- reachable(A,B,G) iff node B is reachable from node A in graph G
reachable(A,B,G) :- transclosure(G,TG), inlist((A,B),TG).


% complete(G) iff G is a complete graph ( (A,B) in G for all points A, B):
complete(Domain,G) :-      
	       nott( (inlist(C1,Domain), inlist(C2,Domain), nott(C1=C2),
	             nott(inlist((C1,C2),G))) ).

% another sample graph:
graph2([(a,c), (c,e), (b,e), (e,d)]).


%  -------------------------------------------------------------------
%  Robust Road Systems

% Want: a network of (2-way) roads connecting a number of towns such that:
% if any road becomes impassable it will still be possible to go from
% any town to any other town.  Such a network of roads is called "robust".

% domain:
towns([hartford,manchester,weathersfield,rockyhill,newington]).

roads([ (hartford,manchester),      
	(hartford,weathersfield),
	(weathersfield,rockyhill),
	(hartford,newington),
	(weathersfield,manchester),
	(newington,manchester),
        (newington,rockyhill) ]).

% graph  (symmetic closure of roads)
twoways(R) :- roads(Rs), symclosure(Rs,R).  % all roads are two-way


safe(Towns,Len,N) :- N > Len.
safe(Towns,Len,N) :- N =< Len,
	roads(Normroads), 
	deleteNth(N,Normroads,R2), 
	symclosure(R2,Newroads),   % forms two-way roads
	transclosure(Newroads,TC), !,  % (! is for efficiency; ignore)
	complete(Towns,TC), !,     % is the reachability relation complete?
	N2 is (N + 1), safe(Towns,Len,N2).

robust(R) :- towns(Ts), length(R,Len), safe(Ts,Len,0).

% goal: twoways(R), robust(R) implies the roads are robust.



% Alternative definition of transitive closure that will not add
% edges of the form (A,A):
trans2(G) :- nott( (inlist((X,Y),G), inlist((Y,Z),G), 
	          nott(X=Z), nott(inlist((X,Z),G))) ).

transclose2(G,G) :- trans2(G).
transclose2(G,TG) :- inlist((X,Y), G), inlist((Y,Z), G), 
	             nott(X=Z), nott(inlist((X,Z), G)), 
		     transclose2([(X,Z)|G], TG).



% utilities

% the following definition of negation is needed in some versions of Prolog
nott(G) :- G, !, 5 = 4.
nott(G).

inlist(X,[X|T]).
inlist(X,[H|T]) :- inlist(X,T).

% deleteNth(N,L,M) iff M is L with the Nth element deleted.
deleteNth(0,L,L).
deleteNth(1,[H|T],T).
deleteNth(N,[H|T],[H|T2]) :- N2 is (N - 1), deleteNth(N2,T,T2).