%%% -*- prolog -*-

%% FACT:
man(aristotle).			% Capitalized = logic variable

%% RULE:
mortal(X) :- man(X).		% read "can conclude <left> when <right>
%% or read: for all X, man(X) implies mortal(X)

%% Terminology:
%% "man" and "mortal" are predicates.  Both are of "arity" 1, written
%% man/1 and mortal/1
%% "aristotle" is a "term".  "Terms" are basically s-expressions.

%% Tell prolog to load a file logic.pl with:
%% > ?- [logic]
%% | ?- mortal(aristotle).	% try to prove this?  (this is a "query")
%% yes				% it is true!
%% | ?- mortal(M).		% try to prove this?  What: exists M s.t. mortal(M)
%% M = aristotle
%% yes

%%% Peano Arithmetic!

%% term z for zero
%% term s(X) for successor of X

zero(z).
%% pred(X,Y) means "predecessor of X is Y"
pred(s(X),X).

%% | ?- pred(s(s(s(s(s(z))))), F), pred(F, T), pred(T, D), pred(D, O).
%% 
%% D = s(s(z))
%% F = s(s(s(s(z))))
%% O = s(z)
%% T = s(s(s(z)))
%% 
%% yes

%% add(X, Y, Z) means "X plus Y is Z"
add(z, X, X).
add(s(X), Y, s(Z)) :- add(X, Y, Z).

%% sub(X,Y,Z) means "X minus Y is Z"
sub(X, Y, Z) :- add(Y, Z, X).

%% CLOSED WORLD ASSUMPTION in action:
%% | ?- sub(s(s(s(z))), s(s(s(s(z)))), X).
%% no

%%% Syntax for lists in
%%% Scheme		Haskell			Prolog
%%%  '()		 []			 []
%%%  '(x y z)            [a,b,c]                 [a,b,c]
%%%  (cons a b)          a:b			 [a|B]
%%%  '(a b c)            a:b:c		 	 [a,b|C]

%% mem(X,Xs) means X is an element of the list Xs.
mem(X, [X|_]).
mem(X, [_|Ys]) :- mem(X, Ys).

%% | ?- mem(X, [abe, bob, cat, doug]), mem(X, [doug, eagan, fiachra]).
%% X = doug ? ;
%% no

%% app(Xs, Ys, Zs) means Xs appended to Ys is Zs (all lists)
app([], Xs, Xs).
app([X|Xs], Ys, [X|Zs]) :- app(Xs, Ys, Zs).

%% different defininition of member
memb(X, Ys) :- app(_, [X|_], Ys).
