element(H,[H|_]). element(X,[_|T]) :- element(X,T). % Mitchell's NELL concepts %===================================================================== % Prover for "D1" transitive mono-dyadic definite clauses prove_d1(P,X,Y,Sig,G1,G2,N,M) :- element(Q,Sig), X@>Y, abduce(rule4_d1(P,Q),G1,G3,N,N1), prove_d1(Q,Y,X,Sig,G3,G2,N1,M). % P(X,Y) <- Q(Y,X) prove_d1(P,X,Y,Sig,G1,G2,N,M) :- Y@>X, abduce(rule11_d1,G1,G3,N,N1), prove_d1(symmetric,P,Sig,G3,G4,s(N1),N2), prove_d1(P,Y,X,Sig,G4,G2,N2,M). % P(X,Y) <- symmetric(P), P(Y,X) prove_d1(P,X,X,Sig,G1,G2,N,M) :- abduce(rule10_d1(P),G1,G2,N,M). % P(X,X) <- 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) :- abduce(rule2_d1(P,X,Y),G1,G2,N,M). % P(X,Y) <- 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,Sig,G1,G2,N,M) :- monadic_d1(P), dyadic_d1(Q), P@>Q, monadic_d1(R), P@>=R, object_d1(Y), Y@>X, abduce(rule9_d1(P,Q,R),G1,G3,N,N1), prove_d1(Q,X,Y,Sig,G3,G4,N1,N2), prove_d1(R,Y,Sig,G4,G2,N2,M). % P(X) <- Q(X,Y), R(Y) prove_d1(P,X,Sig,G1,G2,N,M) :- abduce(rule0_d1(P,X),G1,G2,N,M). % P(X) <- % prove_d1(P,X,Y,Sig,G1,G2,N,M) :- element(Q,Sig), P@>Q, element(R,Sig), % % object_d1(Z), % [P,X,Y] @> [Q,X,Z], [P,X,Y] @> [R,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), R(Z,Y) % % prove_d1(P,X,Y,Sig,G1,G2,N,M) :- element(Q,Sig), P@>Q, element(R,Sig), % % object_d1(Z), % % [P,X,Y] @> [Q,Z,X], [P,X,Y] @> [R,Z,Y], % % abduce(rule8_d1(P,Q,R),G1,G3,N,N1), % % prove_d1(Q,Z,X,Sig,G3,G4,N1,N2), prove_d1(R,Z,Y,Sig,G4,G2,N2,M). % % P(X,Y) <- Q(Z,X), R(Z,Y) % prove_d1(P,X,Y,Sig,G1,G2,N,M) :- element(Q,Sig), % [P,X,Y] @> [Q,X,Y], % 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,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,Y,Sig,G1,G2,N,M) :- element(Q,Sig), element(R,Sig), % [P,X,Y] @> [R,X,Y], [R,X,Y] @> [Q,X], % abduce(rule6_d1(P,R,Q),G1,G3,N,N1), % prove_d1(R,X,Y,Sig,G3,G4,N1,N2), prove_d1(Q,X,Sig,G4,G2,N2,M). % % P(X,Y) <- R(X,Y), Q(X) % % % mode(6,(#P,Q,R [P,X,Y] :- [Q,X],[R,X,Y])). % % prove_d1(P,X,Y,Sig,G1,G2,N,M) :- element(Q,Sig), element(R,Sig), % [P,X,Y] @> [R,X,Y], [R,X,Y] @> [Q,Y], % abduce(rule7_d1(P,R,Q),G1,G3,N,N1), % prove_d1(R,X,Y,Sig,G3,G4,N1,N2), prove_d1(Q,Y,Sig,G4,G2,N2,M). % % P(X,Y) <- R(X,Y), Q(Y) 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), !. % Rule 9 % P(X) <- Q(X,Y), R(Y) pprint1([rule9_d1(P,Q,R)|T]) :- tab(4), write(P), write('(X) :- '), write(Q), write('(X,Y), '), write(R), write('(Y).'), nl, pprint1(T), !. % Rule 10 % P(X,X) <- pprint1([rule10_d1(P)|T]) :- tab(4), write(P), write('(X,X).'), pprint1(T), !. pprint1([rule11_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 examples 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 examples 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,[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) :- episode(E,Pos,Neg,_), length(Pos,P), length(Neg,N), M2 is floor(log(P+N)/log(2))+1, interval(1,M2,I), learn_episode(E,I,Sig,Sig1,BK,Hyp1), learn_seq(T,Sig1,Hyp1,Hyp), !. learn_seq([E|_],_,_,_) :- episode(E,Pos,Neg,_), length(Pos,P), length(Neg,N), M2 is floor(log(P+N)/log(2))+1, % 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=