DonaldKellett

% The words to fill in for the crossword
word(astante, a,s,t,a,n,t,e).
word(astoria, a,s,t,o,r,i,a).
word(baratto, b,a,r,a,t,t,o).
word(cobalto, c,o,b,a,l,t,o).
word(pistola, p,i,s,t,o,l,a).
word(statale, s,t,a,t,a,l,e).

% A specification on how the crossword grid must be filled
crossword(W1, W2, W3, W4, W5, W6) :-

DonaldKellett

% The doll katarina contains the doll olga, which contains the doll natasha, which contains the doll irina
directlyIn(irina, natasha).
directlyIn(natasha, olga).
directlyIn(olga, katarina).

% in(X, Y) represents the statement "Doll X is contained within doll Y"
% Note that this order is the reverse of the exercise description in Learn Prolog now! (where in(X, Y) states "Doll X contains doll Y" instead) but I thought it made more sense this way.
% Doll X is in doll Y if X is directly in Y
in(X, Y) :- directlyIn(X, Y).
% Doll X is in doll Y if X is directly in some doll Z such that Z is in Y

DonaldKellett

% Knowledge base of direct train routes (provided)
% Assumption: such direct train routes are unidirectional, i.e. directTrain(X, Y) does not imply directTrain(Y, X)
directTrain(saarbruecken,dudweiler).
directTrain(forbach,saarbruecken).
directTrain(freyming,forbach).
directTrain(stAvold,freyming).
directTrain(fahlquemont,stAvold).
directTrain(metz,fahlquemont).
directTrain(nancy,metz).

DonaldKellett

% greater_than/2 - Given 2 natural numbers X, Y (as defined by Peano's axioms), is X > Y.
% Basis: The successor of any natural number must be greater than 0
greater_than(succ(_), 0).
% Inductive step: if X > Y, then succ(X) > succ(Y)
greater_than(succ(X), succ(Y)) :- greater_than(X, Y).

DonaldKellett

% swap/2 - Are 2 binary trees X, Y mirror images of each other?
% Basis: Two leaves leaf(X), leaf(Y) are mirror images of each other if X = Y
swap(leaf(X), leaf(X)).
% Inductive Step: If trees L0, R1 are mirror images and L1, R0 mirror images of each other then tree(L0, R0) and tree(L1, R1) are also mirror images of each other.
swap(tree(L0, R0), tree(L1, R1)) :- swap(L0, R1), swap(L1, R0).

DonaldKellett

% A directed graph (provided)
connected(1,2).
connected(3,4).
connected(5,6).
connected(7,8).
connected(9,10).
connected(12,13).
connected(13,14).
connected(15,16).
connected(17,18).

DonaldKellett

% Knowledge base of travel information (provided)
% Assumption: these routes are unidirectional
byCar(auckland,hamilton).
byCar(hamilton,raglan).
byCar(valmont,saarbruecken).
byCar(valmont,metz).

byTrain(metz,frankfurt).
byTrain(saarbruecken,frankfurt).
byTrain(metz,paris).

DonaldKellett

% Knowledge base of travel routes (provided)
% Assumption: these routes are unidirectional
byCar(auckland,hamilton).
byCar(hamilton,raglan).
byCar(valmont,saarbruecken).
byCar(valmont,metz).

byTrain(metz,frankfurt).
byTrain(saarbruecken,frankfurt).
byTrain(metz,paris).

DonaldKellett

% Knowledge base of travel routes (provided)
% Assumption: these routes are unidirectional
byCar(auckland,hamilton).
byCar(hamilton,raglan).
byCar(valmont,saarbruecken).
byCar(valmont,metz).

byTrain(metz,frankfurt).
byTrain(saarbruecken,frankfurt).
byTrain(metz,paris).

DonaldKellett

second(X, [_, X | _]).