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

%=====================================================================
% Prover for "D1" transitive mono-dyadic definite clauses

prove_d1(P,X,Y,Sig,G1,G2,N,M) :- element(Q,Sig), P@>Q,
		abduce(rule3_d1(P,Q),G1,G3,N,N1),
		prove_d1(Q,X,Y,Sig,G3,G2,N1,M).
					% P(X,Y) <- Q(X,Y)
prove_d1(P,X,Y,Sig,G1,G2,N,M) :- element(Q,Sig), P@>Q, element(R,Sig), P@>=R,
		object_d1(Z), X @> Z, Z@> Y,
		abduce(rule5_d1(P,Q,R),G1,G3,N,N1), 
		prove_d1(Q,X,Z,Sig,G3,G4,N1,N2), prove_d1(R,Z,Y,Sig,G4,G2,N2,M).
					% P(X,Y) <- Q(X,Z), P(Z,Y)

%=====================================================================


prove_d1(P,X,Y,Sig,G1,G2,N,M) :- Y@>X,
		abduce(rule9_d1,G1,G3,N,N1),
		prove_d1(symmetric,P,Sig,G3,G4,N1,N2),
		prove_d1(P,Y,X,Sig,G4,G2,N2,M).
					% P(X,Y) <- symmetric(P), P(Y,X)
prove_d1(P,X,Y,Sig,G1,G2,N,M) :-
		abduce(rule2_d1(P,X,Y),G1,G2,N,M).
					% P(X,Y) <-
prove_d1(P,X,Sig,G1,G2,N,M) :- element(Q,Sig),
		[P,X] @> [Q,X],
		abduce(rule1_d1(P,Q),G1,G3,N,N1),
		prove_d1(Q,X,Sig,G3,G2,N1,M).
					% P(X) <- Q(X)
prove_d1(P,X,Sig,G1,G2,N,M) :-
 			abduce(rule0_d1(P,X),G1,G2,N,M).	% P(X) <-

% Example
%	b_male(i_harry).					% Rule0
%	b_male(n_john).						% Rule0
%	c_female(j_susan).					% Rule0
%	d_person(X) :- b_male(X).				% Rule1
%	g_father(n_john,i_harry).				% Rule2
%	g_father(n_john,j_susan).				% Rule2
%	h_brother(n_john,m_bill).				% Rule2
%	j_child(i_harry,n_john).				% Rule2
%	i_parent(X,Y) :- g_father(X,Y).				% Rule3
%	j_child(X,Y) :- i_parent(Y,X).				% Rule4
%	l_uncle(X,Y) :- i_parent(X,Z), bother(Z,Y).		% Rule5
%	k_son(X,Y) :- j_child(X,Y), b_male(Y).			% Rule7

monadic_d1(b_male).
monadic_d1(c_female).
monadic_d1(d_person).
monadic_d1(X) :- skolem_p(X).
dyadic_d1(X) :- skolem_p(X).
dyadic_d1(f_mother).
dyadic_d1(g_father).
% dyadic_d1(h_brother).
% dyadic_d1(i_parent).
% dyadic_d1(j_child).
% dyadic_d1(k_son).
% dyadic_d1(l_uncle).
% dyadic_d1(m_grandfather).
% dyadic_d1(n_grandmother).
dyadic_d1(o_grandparent).
dyadic_d1(p_greatgrandparent).
% dyadic_d1(q_ancestor).

object_d1(a_bob).
object_d1(b_jane).
object_d1(c_sam).
object_d1(d_jo).
object_d1(e_jill).
object_d1(f_ted).
object_d1(g_megan).
object_d1(h_liz).
object_d1(i_harry).
object_d1(j_susan).
object_d1(k_andy).
object_d1(l_alice).
object_d1(m_bill).
object_d1(n_john).
object_d1(o_mary).
object_d1(p_jake).
object_d1(q_matilda).
object_d1(X) :- skolem_r(X).

rule0_d1(b_male,i_harry).
rule0_d1(b_male,n_john).
rule0_d1(b_male,m_bill).
rule0_d1(c_female,j_susan).
rule0_d1(c_female,q_matilda).
% rule1_d1(d_person,b_male).
% rule2_d1(g_father,p_jake,m_bill).
rule2_d1(g_father,p_jake,l_alice).
rule2_d1(g_father,p_jake,n_john).
rule2_d1(g_father,n_john,h_liz).
rule2_d1(g_father,n_john,i_harry).
rule2_d1(g_father,n_john,j_susan).
rule2_d1(g_father,n_john,k_andy).
rule2_d1(g_father,m_bill,f_ted).
rule2_d1(g_father,m_bill,g_megan).
rule2_d1(g_father,i_harry,c_sam).
rule2_d1(g_father,i_harry,d_jo).
rule2_d1(g_father,f_ted,a_bob).
rule2_d1(g_father,f_ted,b_jane).
rule2_d1(f_mother,q_matilda,m_bill).
rule2_d1(f_mother,q_matilda,l_alice).
rule2_d1(f_mother,q_matilda,n_john).
rule2_d1(f_mother,l_alice,f_ted).
rule2_d1(f_mother,l_alice,g_megan).
rule2_d1(f_mother,o_mary,i_harry).
rule2_d1(f_mother,o_mary,j_susan).
rule2_d1(f_mother,o_mary,k_andy).
rule2_d1(f_mother,e_jill,a_bob).
rule2_d1(f_mother,e_jill,b_jane).
rule2_d1(f_mother,h_liz,c_sam).
rule2_d1(f_mother,h_liz,d_jo).
rule2_d1(h_brother,m_bill,n_john).
rule2_d1(h_brother,k_andy,j_susan).
rule2_d1(h_brother,k_andy,i_harry).
rule2_d1(hh_sister,j_susan,i_harry).
rule2_d1(hh_sister,j_susan,h_liz).
rule2_d1(j_child,i_harry,n_john).
rule2_d1(j_child,j_susan,n_john).
% rule2_d1(i_parent,n_john,i_harry).
% rule2_d1(i_parent,i_harry,c_sam).
% rule3_d1(i_parent,g_father).
rule4_d1(j_child,i_parent).
% rule5_d1(l_uncle,i_parent,h_brother).
% rule7_d1(k_son,j_child,b_male).
% rule9_d1.

% skolem_p(e_p0).
skolem_p(h_p1).
% skolem_p(h_p2).
% skolem_p(z_p1).

skolem_o(o0).
% skolem_o(o1).

abduce(X,G,G,N,N) :- X, !.
abduce(X,G,G,N,N) :- element(X,G), !.
abduce(X,G,[X|G],s(N),N) :- not(element(X,G)), !.

% Pretty print rules

pprint(G) :- nl, nl, pprint1(G). % Print Prolog clauses

pprint1([]) :- nl, !.   % Print Production Rules
pprint1([rule0_d1(P,X)|T]) :-
        tab(4), write(P), write('('), write(X), write(').'), nl,
        pprint1(T), !.
pprint1([rule1_d1(P,Q)|T]) :-
        tab(4), write(P), write('(X) :- '), write(Q), write('(X).'), nl,
        pprint1(T), !.
pprint1([rule2_d1(P,X,Y)|T]) :-
        tab(4),
	write(P), write('('), write(X), write(','), write(Y), write(').'), nl,
        pprint1(T), !.
pprint1([rule3_d1(P,Q)|T]) :-
        tab(4),
	write(P), write('(X,Y) :- '), write(Q), write('(X,Y).'), nl,
        pprint1(T), !.
pprint1([rule4_d1(P,Q)|T]) :-
        tab(4),
	write(P), write('(X,Y) :- '), write(Q), write('(Y,X).'), nl,
        pprint1(T), !.
pprint1([rule5_d1(P,Q,R)|T]) :-
        tab(4),
	write(P), write('(X,Y) :- '),
	write(Q), write('(X,Z), '),
	write(R), write('(Z,Y).'), nl,
        pprint1(T), !.
% Rule 6 						% P(X,Y) <- R(X,Y), Q(X)
pprint1([rule6_d1(P,Q,R)|T]) :-
        tab(4),
	write(P), write('(X,Y) :- '),
	write(Q), write('(X,Y), '),
	write(R), write('(X).'), nl,
        pprint1(T), !.
% Rule 7						% P(X,Y) <- R(X,Y), Q(Y)
pprint1([rule7_d1(P,Q,R)|T]) :-
        tab(4),
	write(P), write('(X,Y) :- '),
	write(Q), write('(X,Y), '),
	write(R), write('(Y).'), nl,
        pprint1(T), !.
% Rule 8						% P(X,Y) <- R(Z,X), Q(Z,Y)
pprint1([rule8_d1(P,Q,R)|T]) :-
        tab(4),
	write(P), write('(X,Y) :- '),
	write(Q), write('(Z,X), '),
	write(R), write('(Z,Y).'), nl,
        pprint1(T), !.
pprint1([rule9_d1|T]) :-			% P(X,Y) <- symmetric(P), P(Y,X)
        tab(4),
	write('P(X,Y) <- symmetric(P), P(Y,X)'), nl,
        pprint1(T), !.
					

reverse(L,R) :- reverse1(L,R,[]).       % Reverse a list

reverse1([],L,L) :- !.
reverse1([H|T],R,L) :- reverse1(T,R,[H|L]), !.


prove_d0(P,X,Sig,G,G,N,N) :-
	prove_d1(P,X,Sig,G,G,N,N), !.	% Deductive proof Monadic
prove_d0(P,X,Sig,G1,G3,N,N1) :-
	prove_d1(P,X,Sig,G1,G3,N,N1). % Abductive proof Monadic
prove_d0(P,X,Y,Sig,G,G,N,N) :-
	prove_d1(P,X,Y,Sig,G,G,N,N), !. % Deductive proof Dyadic
prove_d0(P,X,Y,Sig,G1,G3,N,N1) :-
	prove_d1(P,X,Y,Sig,G1,G3,N,N1). % Abductive proof Dyadic


proveall([],_,G,G,N) :- !.       % Find G that fits all the positive epsisodes
proveall([[P,X]|T],Sig,G1,G2,N) :-
        prove_d0(P,X,Sig,G1,G3,N,N1),
	write('EXAMPLE:'), pprint([rule0_d1(P,X)]),
	write('HYPOTHESIS: ['), peano(N0,N1), write(N0),
		write(' clauses left]'), pprint(G3),
        proveall(T,Sig,G3,G2,N1).
proveall([[P,X,Y]|T],Sig,G1,G2,N) :-
        prove_d1(P,X,Y,Sig,G1,G3,N,N1),
	write('EXAMPLE:'), pprint([rule2_d1(P,X,Y)]),
	write('HYPOTHESIS: ['), peano(N0,N1), write(N0),
		write(' clauses left]'), pprint(G3),
        proveall(T,Sig,G3,G2,N1).

nproveall([],_,_) :- !.       % Check G fits all the negative epsisode
nproveall([[P,X]|T],Sig,G) :-
        not(prove_d1(P,X,Sig,G,G,0,0)),
        nproveall(T,Sig,G), !.
nproveall([[P,X,Y]|T],Sig,G) :-
        not(prove_d1(P,X,Y,Sig,G,G,0,0)),
        nproveall(T,Sig,G), !.

% Generate a Peano number

peano(0,0) :- !.
peano(N,s(M)) :- not(var(N)), !, N1 is N-1, peano(N1,M), !.
peano(N,s(M)) :- var(N), !, peano(N1,M), N is N1+1, !.

append([],L,L).
append([H|T],L,[H|R]) :- append(T,L,R).

reverse(L1,L2) :- reverse1(L1,[],L2).

reverse1([],L,L) :- !.
reverse1([H|T],[H|R],L) :- reverse1(T,R,L).

% rev_union builds the union of the two signatures in reverse sorted order

rev_union(Sig1,Sig2,Sig3) :-
	append(Sig1,Sig2,Sig4),
	sort(Sig4,Sig5),
	reverse(Sig5,Sig3), !.

% Extract the signature from background atoms

sig_extract([],Sig,Sig) :- !.
sig_extract([Rule|T],Sig,Sig1) :-
	Rule =.. [Rule],
	sig_extract(T,Sig,Sig1), !.
sig_extract([Rule|T],Sig,[P|Sig1]) :-
	arg(1,Rule,P),
	sig_extract(T,Sig,Sig1), !.

% Learn from sequence of example episodes, where theory size is bounded
% 	by episode size/2.

learn_seq([],_,B,B) :- !.
learn_seq([E|T],Sig,BK,Hyp) :-
	epsisode(E,Pos,Neg,_), length(Pos,P), length(Neg,N),
	M2 is floor(log(P+N)/log(2)), interval(1,M2,I),
	learn_episode(E,I,Sig,Sig1,BK,Hyp1),
	learn_seq(T,Sig1,Hyp1,Hyp), !.
learn_seq([E|_],_,_,_) :-
	epsisode(E,Pos,Neg,_), length(Pos,P), length(Neg,N),
	M2 is floor(log(P+N)/log(2)),	% Logarithmic clause bound
	write('EPISODE '), write(E),
	write(': NO COMPRESSION FOR CLAUSE BOUND UP TO '), write(M2), nl, nl.

interval(Lo,Hi,[Lo|T]) :-
	Lo=<Hi, Lo1 is Lo+1,
	interval(Lo1,Hi,T), !.
interval(_,_,[]).

% Learn from a single example episode and update the signature

learn_episode(Tag,Int,Sig,Sig5,B1,B2) :-
	write('EXAMPLE EPISODE: '), write(Tag), nl, nl,
	epsisode(Tag,Pos,Neg,Sig1),
	rev_union(Sig,Sig1,Sig2),	% Combine signatures
	element(N,Int), peano(N,Lim),
	write('TRY CLAUSE BOUND: '), write(N), nl, nl,
        proveall(Pos,Sig2,B1,B2,Lim), nproveall(Neg,Sig2,B2),
	sig_extract(B2,Sig2,Sig3),	% Extract new signature
	sort(Sig3,Sig4), reverse(Sig4,Sig5),
	write('FINAL HYPOTHESIS FOR EPISODE: '),  write(Tag),
	write(', BOUND: '), write(N),
	pprint(B2), !.

epsisode(parent,   % Learn parent
	[
	 [i_parent,p_jake,l_alice],
	 [i_parent,l_alice,f_ted],
	 [i_parent,m_bill,g_megan],
	 [i_parent,l_alice,f_ted]
	],
	[
         [g_father,l_alice,f_ted]           	% Negatives
	],
	[g_father,f_mother]).			% Initial signature
epsisode(gparent,             % Learn grandparent with eager invention
       [
        [o_grandparent,p_jake,f_ted],   % Positives
        [o_grandparent,n_john,c_sam],
        [o_grandparent,o_mary,c_sam],
        [o_grandparent,q_matilda,g_megan],
        [o_grandparent,l_alice,a_bob],
        [o_grandparent,l_alice,b_jane],
        [o_grandparent,m_bill,a_bob],
        [o_grandparent,m_bill,b_jane]
        ],
       [
        [g_father,l_alice,f_ted]],              % Negatives
       [i_a1,g_father,f_mother]).               % Initial signature
epsisode(ggparent,   % Learn greatgrandparent/grandparent with eager
                        % invention. Corresponds to mixed BOTTOM-UP
                        % and TOP-DOWN PROGRAMMING
       [
        [p_greatgrandparent,p_jake,c_sam],   % Positives
        [p_greatgrandparent,p_jake,d_jo],
        [p_greatgrandparent,q_matilda,c_sam],
        [p_greatgrandparent,q_matilda,d_jo],

        [p_greatgrandparent,p_jake,a_bob],
        [p_greatgrandparent,p_jake,b_jane],
        [p_greatgrandparent,q_matilda,a_bob],
        [p_greatgrandparent,q_matilda,b_jane]
        ],
       [
        [g_father,l_alice,f_ted]],              % Negatives
       [o_a1]).
epsisode(ancestor,   % Learn ancestor
	[
	 [q_ancestor,n_john,c_sam],
	 [q_ancestor,p_jake,l_alice],
	 [q_ancestor,q_matilda,c_sam],
	 [q_ancestor,l_alice,f_ted],
	 [q_ancestor,o_mary,c_sam],
	 [q_ancestor,p_jake,a_bob]
	],
	[],
	[q_ancestor,h_p1,g_father,f_mother]).
epsisode(sibling,  				% Sibling
	[
	 [z_sibling,k_andy,j_susan],
	 [z_sibling,k_andy,i_harry],
	 [z_sibling,j_susan,i_harry],
	 [z_sibling,j_susan,h_liz]
	],
	[[hh_sister,k_andy,j_susan]],
	[h_brother,hh_sister]).
epsisode(sibsym,  				% Sibling
	[
	 [z_sibling,j_susan,k_andy],
	 [z_sibling,i_harry,k_andy],
	 [z_sibling,i_harry,j_susan],
	 [z_sibling,h_liz,j_susan]
	],
	[[hh_sister,k_andy,j_susan]],
	[]).