/*----------------------------------------------------------*/
/*  Coverings, generalizations, lgg's (Sicstus Prolog V2+)  */
/*----------------------------------------------------------*/
/*  (C) 1998 Zdravko Markov                                 */
/*----------------------------------------------------------*/
/* This file contains a collection of various predicates    */
/* implementing covering (subsumption) relations between    */
/* examples and hypotheses in propositional and relational  */
/* representation.                                          */ 
/* The attribute-value rerpesentation of the examples is:   */
/* [A1=V1,...,An=Vn] for nominal attributes and             */
/* [V1,V2,...,Vn]    for structural attributes              */
/*----------------------------------------------------------*/
/*----------------------------------------------------------*/
/*  Attribute-value syntactic covering by dropping condition*/
/*  covers(+H1,+H2)                                         */
/*----------------------------------------------------------*/
covers(H1,H2) :- 
    subset(H1,H2).
/*----------------------------------------------------------*/
/*  Attribute-value genaralization by dropping condition    */
/*  (genarates all generalizations on backtracking)         */
/*  generalize(+H1,-H2)                                     */  
/*----------------------------------------------------------*/
generalize(H1,H2) :-
    length(H1,N),
    template(H2,N),
    sublist(H2,H1).

temlpate(_,0) :- !,fail.
template([_],_).
template([_|T],N) :-
    M is N-1,
    template(T,M).

sublist([X],[X|_]).
sublist(X,[_|T]) :-
    sublist(X,T).
sublist([X|T],[X|V]) :-
    sublist(T,V).
/*----------------------------------------------------------*/
/*  Attribute-value model of a hypothesis                   */
/*  model(+Hypothesis,-Model)                               */
/*----------------------------------------------------------*/
model(H,M) :-
    findall(N,(example(N,_,L),covers(H,L)),M).
/*----------------------------------------------------------*/
/*  Attribute-value semantic covering                       */
/*  sem_covers(+H1,+H2)                                     */
/*----------------------------------------------------------*/
sem_covers(H1,H2) :-
    model(H1,M1),
    model(H2,M2),
    subset(M2,M1).
/*----------------------------------------------------------*/
/*  Attribute-value least general generalization (lgg)      */
/*  by dropping condition                                   */
/*  lgg(+H1,+H2,-LGG)                                       */
/*----------------------------------------------------------*/
lgg(H1,H2,LGG) :-
    intersection(H1,H2,LGG).
/*----------------------------------------------------------*/
/*  Attribute-value sintactic covering by using taxonomies  */
/*  scoves(+H1,+H2)                                         */
/*----------------------------------------------------------*/
scovers([],[]).
scovers([X|T],[Y|L]) :-
     isa(Y,X),
scovers(T,L).
/*----------------------------------------------------------*/
/*  Attribute-value model for structural attributes         */
/*  smodel(+Hypothesis,-Model)                              */
/*----------------------------------------------------------*/
smodel(H,M) :-
    findall(X,scovers(H,X),M).
/*----------------------------------------------------------*/
/*  Attribute-value least general generalization (lgg)      */
/*  by using taxonomies - son(Child,Parent)                 */
/*  slgg(+H1,+H2,-LGG)                                      */
/*----------------------------------------------------------*/
slgg([],[],[]) .
slgg([X|T],[Y|L],[Z|V]) :-
     lge(X,Y,Z),
     slgg(T,L,V).

/*----------------------------------------------------------*/
/*  Check for term subsumption by unification               */
/*  substitution(+Term1,+Term2,-Substitution)               */
/*----------------------------------------------------------*/
substitution(Term1,Term2,Sub_List) :-
     subsumes(Term1,Term2),
     substitute([Term1],[Term2],Subst),
     remove_id(Subst,Sub_List), !.

subsumes(T1,T2) :-
    \+(\+((numbervars(T2,0,_),T1=T2))).

substitute([],[],[]) :- !.
substitute([Head1|Tail1],[Head2|Tail2],[(Head1 / Head2)|Tail3]) :-
     var(Head1),
     substitute(Tail1,Tail2,Tail3), !.
substitute([Head1|Tail1],[Head2|Tail2],Subst) :-
     Head1 =.. [F1|Tail11],
     Head2 =.. [F1|Tail22],
     substitute(Tail11,Tail22,Tail33),
     substitute(Tail1,Tail2,Tail4),
     append(Tail33,Tail4,Subst), !.

remove_id([],[]) :- !.
remove_id([X],[X]) :- !.
remove_id([A,B|Tail],List) :-
     A == B,
     remove_id([A|Tail],List), !.
remove_id([Head1|Tail1],[Head1|Tail2]) :-
     remove_id(Tail1,Tail2), !.

/*----------------------------------------------------------*/
/*  Antiunification (lgg) of terms                          */
/*  anti_unify(+Term1,+Term2,-Term)                         */
/*----------------------------------------------------------*/
anti_unify(Term1,Term2,Term):-
    anti_unify(Term1,Term2,Term,[],S1,[],S2).

anti_unify(Term1,Term2,Term1,S1,S1,S2,S2):-
    Term1 == Term2,!.
anti_unify(Term1,Term2,V,S1,S1,S2,S2):-
    subs_lookup(S1,S2,Term1,Term2,V),!.
anti_unify(Term1,Term2,Term,S10,S1,S20,S2):-
    nonvar(Term1),nonvar(Term2),
    functor(Term1,F,N),functor(Term2,F,N),!,
    functor(Term,F,N),
    anti_unify_args(N,Term1,Term2,Term,S10,S1,S20,S2).
anti_unify(Term1,Term2,V,S10,[Term1-V|S10],S20,[Term2-V|S20]).

anti_unify_args(0,Term1,Term2,Term,S1,S1,S2,S2).
anti_unify_args(N,Term1,Term2,Term,S10,S1,S20,S2) :-	
    N>0,N1 is N-1,
    arg(N,Term1,Arg1),
    arg(N,Term2,Arg2),
    arg(N,Term,Arg),
    anti_unify(Arg1,Arg2,Arg,S10,S11,S20,S21),
    anti_unify_args(N1,Term1,Term2,Term,S11,S1,S21,S2).

subs_lookup([T1-V|Subs1],[T2-V|Subs2],Term1,Term2,V):-
    T1 == Term1,
    T2 == Term2,!.
subs_lookup([S1|Subs1],[S2|Subs2],Term1,Term2,V):-
    subs_lookup(Subs1,Subs2,Term1,Term2,V).
/*----------------------------------------------------------*/
/*  Theta-subsumption check for Horn clauses                */
/*  theta_subsumes(+(H1:-B1),+(H2:-B2)),                    */
/*  where Bi=[L1,...,Ln], Li - literals                     */
/*----------------------------------------------------------*/
theta_subsumes((H1:-B1),(H2:-B2)):-
    \+((H1=H2,ground(B2),\+(subset(B1,B2)))).

ground(Term):-
	numbervars(Term,0,N).
/*----------------------------------------------------------*/
/*  Lgg under theta-subsumption for Horn clauses            */
/*  theta_lgg(+(H1:-B1),+(H2:-B2),-(H:-B)),                 */
/*  where Bi=[L1,...,Ln], Li - literals                     */
/*----------------------------------------------------------*/
theta_lgg((H1:-B1),(H2:-B2),(H:-B)):-
    anti_unify(H1,H2,H,[],S10,[],S20),
    theta_lgg_bodies(B1,B2,[],B,S10,S1,S20,S2).

theta_lgg_bodies([],B2,B,B,S1,S1,S2,S2).
theta_lgg_bodies([L|B1],B2,B0,B,S10,S1,S20,S2):-
    theta_lgg_literal(L,B2,B0,B00,S10,S11,S20,S21),
    theta_lgg_bodies(B1,B2,B00,B,S11,S1,S21,S2).

theta_lgg_literal(L1,[],B,B,S1,S1,S2,S2).
theta_lgg_literal(L1,[L2|B2],B0,B,S10,S1,S20,S2):-
    same_predicate(L1,L2),
    anti_unify(L1,L2,L,S10,S11,S20,S21),
    theta_lgg_literal(L1,B2,[L|B0],B,S11,S1,S21,S2).
theta_lgg_literal(L1,[L2|B2],B0,B,S10,S1,S20,S2):-
    \+(same_predicate(L1,L2)),
    theta_lgg_literal(L1,B2,B0,B,S10,S1,S20,S2).

/*----------------------------------------------------------*/
/*  Auxilliary predicates                                   */
/*----------------------------------------------------------*/
isa(X,X) .
isa(X,Y) :-
     son(X,Z),
     isa(Z,Y).

lge(X1,X2,X1) :-
     isa(X2,X1), !.
lge(X1,X2,L) :-
     son(X1,F),
     lge(F,X2,L).

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

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

subset([],_).
subset([X|T],L) :- 
    member(X,L), !, 
    subset(T,L).

intersection([],_,[]).
intersection([X|T],L,[X|V]) :- 
    member(X,L), !, 
    intersection(T,L,V).
intersection([_|T],L,V) :- 
    intersection(T,L,V).

same_predicate(L1,L2):-
    functor(L1,P,N),functor(L2,P,N).