/******************************************************************/ 
/* foil.pl                                                        */ 
/* Quinlan's First-Order Inductive Learning of relational concepts*/ 
/******************************************************************/ 
%  http://www.cs.ccsu.edu/~markov/ccsu_courses/mlprograms/
%
% 
%    Copyright 1991 by John M. Zelle and Raymond J. Mooney 
% 
%    Permission to use this software is granted subject to the 
%    following restrictions and understandings: 
% 
%    1. This material is for educational and research purposes only. 
% 
%    2. Raymond J. Mooney has provided this software AS IS. Raymond 
%       J. Mooney has made no warranty or representation that the 
%       operation of this software will be error-free, and he is 
%       under no obligation to provide any services, by way of 
%       maintenance, update, or otherwise. 
% 
%    3. Any user of such software agrees to indemnify and hold 
%       harmless Raymond J. Mooney and The University of Texas from 
% all claims arising out of the use or misuse of this 
% software, or arising out of any accident, injury, or damage 
% whatsoever, and from all costs, counsel fees and liabilities 
%       incurred in or about any such claim, action, or proceeding 
%       brought thereon. 
% 
%    4. Users are requested, but not required, to inform Raymond J. 
% Mooney of any noteworthy uses of this software. 
% 
%    5. All materials and reports developed as a consequence of the 
%       use of this software shall duly acknowledge such use, in 
% accordance with the usual standards of acknowledging credit 
% in academic research. 
% 
/******************************************************************/ 
/*                                                                */ 
/*  impl. by    : John M. Zelle                                   */ 
/*                1992                                            */ 
/*                                                                */ 
/*  reference   : Learning Logical Definitions from Relations,    */ 
/*                Quinlan, J. R., Machine Learning, 5, 1990.      */ 
/*                                                                */ 
/*                Determinate Literals in Inductive Logic         */ 
/*                Programming, Quinlan, J. R., Proceedings of the */ 
/*                Eighth International Workshop in Machine        */ 
/*                Learning, 1991                                  */ 
/*                                                                */ 
/*  call        : foil(Name/Arity),                               */ 
/*                foil(Predicate),                                */ 
/*                                                                */ 
/*  parameter   : foil_predicates/1, foil_use_negations/1,        */ 
/*                foil_det_lit_bound/1, foil_cwa/1                */ 
/*                                                                */ 
/******************************************************************/ 
/* The version presented here is somewhat simplified in that it   */ 
/* uses a much weaker test to constrain recursive predicates (a   */ 
/* recursive call must contain vars not found in the head of a    */ 
/* clause, and may not introduce any unbound vars), and it does   */ 
/* not incorporate encoding length restrictions to handle noisy   */ 
/* data. There is also no post-processing of clauses to simplify  */ 
/* learned definitions, although this would be relatively easy to */ 
/* add.                                                           */ 
/*                                                                */ 
/* This is a very simple implementation which recomputes tuple    */ 
/* sets "on the fly".  Don't expect it to run like the wind.      */ 
/*                                                                */ 
/* The background knowledge for predicate induction is represented*/ 
/* as "existential" predicates. By existential it is meant that   */ 
/* the definitions there must be fully constructive to avoid      */ 
/* instantiation errors when running FOIL. The input data file    */ 
/* needs to be preceeded by the following header (see also the    */ 
/* example files):                                                */ 
/*                                                                */ 
/*  foil_predicates(<FunctorList>).                               */ 
/*  foil_cwa(<Boolean>).                                          */  
/*  foil_use_negations(<Boolean>).                                */ 
/*  foil_det_lit_bound(<Integer>).                                */ 
/*----------------------------------------------------------------*/
/* default values                                                 */

   foil_use_negations(false).
   foil_det_lit_bound(0).

/*----------------------------------------------------------------*/
/* were foil_predicates(<FunctorList>) declares all predicates    */ 
/* occuring in FunctorList, which are used in the example facts.  */ 
/* If foil should use the closed world assumption, foil_cwa must  */ 
/* be set to true. Otherwise, explicitly asserted negative facts  */ 
/* (for the relation in question) are used if they exist. Whether */ 
/* Foil should use negated literals in the body of generated      */ 
/* clauses can be switched on or off with the fact                */ 
/* foil_use_negations(<Boolean>), its argument can be either true */ 
/* or false. And foil_det_lit_bound(<Integer>) is used as depth   */ 
/* limit on the search for determinate literals.                  */ 
/******************************************************************/ 
% This is YAP- and SWI-Prolog specific 

log(X,Y) :- 
 Y is log(X). 

/******************************************************************/ 
/*                                                                */ 
/*  call        : foil (+PREDICATE)                               */ 
/*                                                                */ 
/*  arguments   : PREDICATE = Either a most general predicate or  */ 
/*                            a Prolog functor                    */ 
/*                            e.g. predicate(_,_) or predicate/2  */ 
/*                                                                */ 
/******************************************************************/ 
/* Run FOIL to attempt finding a definition for PREDICATE and     */ 
/* then print out the resulting clauses.                          */ 
/******************************************************************/ 
foil(Name/Arity) :- 
 functor(Predicate,Name,Arity), 
 !, 
 foil(Predicate). 
foil(Goal) :- 
 foil(Goal,Clauses), 
 nl, write('Found definition:'), nl, 
 portray_clauses(Clauses). 
 
 
portray_clauses([]) :- 
 nl. 
portray_clauses([H|T]):- 
 portray_clause(H), 
 portray_clauses(T). 
 
 
% Clauses is the set of clauses defining Goal found by FOIL. Negative 
% examples are provided by either explicitly or by closed world 
% assumption on the Herbrand base, depending in the switch foil_cwa/1. 
foil(Goal, Clauses) :- 
 get_examples(Goal, Positives, Negatives), 
 foil_loop(Positives, Goal, Negatives, [], Clauses). 
 
 
% Find the positive and negative examples of Goal. Negative examples 
% are constructed using the closed world assumption, if foil_cwa is 
% set to true, otherwise explicitly given negative examples for Goal 
% are used. 
get_examples(Goal, Pos, Neg) :- 
 findall(Goal, clause(Goal,true), Pos), 
 ( foil_cwa(true) -> 
       create_negatives(Pos, Neg) 
 ; findall(Goal, clause(neg(Goal),true), Neg) 
 ). 
 
 
/******************************************************************/ 
/*                                                                */ 
/*  call        : foil_loop (+POSITIVE,+GOAL,+NEGATIVE,+ACCU,     */ 
/*        -CLAUSES)                            */ 
/*                                                                */ 
/*  arguments   : POSTITIVE = Positive examples left to be covered*/ 
/*                GOAL      = The predicate which should be       */ 
/*                            defined.                            */ 
/*                NEGATIVE  = Negative examples of GOAL           */ 
/*                ACCU      = Clauses found in previous iterations*/ 
/*                CLAUSES   = Resulting clauses defining GOAL     */ 
/*                                                                */ 
/******************************************************************/ 
/* This predicate corresponds to the "outer loop" in Quinlan 90.  */ 
/* Each iteration of the outer loop attempts to construct a       */ 
/* clause, printsit and determines the remaining set of positive  */ 
/* examples for the next iteration. If no positive examples are   */ 
/* left, the outer loop terminates, and the set of clauses        */ 
/* defining GOAL is given back as result.                         */ 
/******************************************************************/ 
foil_loop(Pos, Goal, Neg, Clauses0, Clauses) :- 
 ( Pos = [] -> 
       Clauses = Clauses0 
 ; nl, write('Uncovered positives:'), nl, 
   write(Pos), nl, 
   nl, write('Adding a clause ...'), nl, nl, 
   extend_clause_loop(Neg, Pos, (Goal :- true), Clause), 
   nl, write('Clause found:'), nl, 
   portray_clause(Clause), 
   uncovered_examples(Clause, Pos, Pos1), 
   foil_loop(Pos1, Goal, Neg, [Clause|Clauses0], Clauses) 
 ). 
 
/******************************************************************/ 
/*                                                                */ 
/*  call        : extend_clause_loop (+NEGATIVE,+POSITIVE,+SEED,  */ 
/*                 -CLAUSE)                    */ 
/*                                                                */ 
/*  arguments   : NEGATIVE  = Negative examples of GOAL           */ 
/*                POSTITIVE = Positive examples left to be covered*/ 
/*                SEED      = The most general clause defining    */ 
/*                            the predicate.                      */ 
/*                CLAUSE    = The extended clause which covers no */ 
/*                            negative examples, or which cannot  */ 
/*                            be improved.                        */ 
/*                                                                */ 
/******************************************************************/ 
/* This predicate corresponds to the "inner loop" in Quinlan 90   */ 
/* and in a general to specific manner. At each iteration a       */ 
/* premises is determined and added to SEED, until it covers no   */ 
/* negative examples, or until the information gain does not      */ 
/* improve. If the latter happens, determinate literals may be    */ 
/* added to the clause (see Quinlan 91), depending on the value   */ 
/* of the switch foil_det_lit_bound/1. This switch determines the */ 
/* maximum number of determinate literals which can be added to   */ 
/* the clause.                                                    */ 
/******************************************************************/ 
extend_clause_loop(Nxs0, Pxs0, Clause0, Clause) :- 
 ( Nxs0 = [] -> 
       Clause = Clause0 
 ; write('Specializing current clause: '), nl, 
   portray_clause(Clause0), 
   nl, write('Covered negatives:'), nl, write(Nxs0), nl, 
   nl, write('Covered positives:'), nl, write(Pxs0), nl, nl, 
   generate_possible_extensions(Clause0, Ls), 
   info_value(Clause0, Pxs0, Nxs0, Info), 
   best_next_clause(Ls, Nxs0, Pxs0, Clause0, Info, 0, Clause0, Clause1), 
   ( Clause0 == Clause1 -> 
  foil_det_lit_bound(DLB), 
  nl, 
  write('No improvement -- trying determinate literals ...'), nl, 
  bounded_determinate_literals(DLB, Ls, Clause0, Pxs0, Nxs0, Ds), 
  ( Ds = [] -> 
        write('No determinate literals found.'), nl, 
        covered_examples(Clause1, Nxs0, Nxs1), 
        write('WARNING -- clause covers negatives:'), nl, 
        write(Nxs1), nl, 
        Clause = Clause1 
  ; write('Adding determinate literals: '), write(Ds), nl, 
    add_literals(Ds, Clause0, Clause2), 
    covered_examples(Clause2, Nxs0, Nxs1), 
    extend_clause_loop(Nxs1, Pxs0, Clause2, Clause) 
  ) 
   ; covered_examples(Clause1, Pxs0, Pxs1), 
     covered_examples(Clause1, Nxs0, Nxs1), 
     extend_clause_loop(Nxs1, Pxs1, Clause1, Clause) 
   ) 
 ). 
  
% Compute the information matric for the set of positive and negative 
% tuples which result from applying Clause to the examples Pxs and 
% NXs. 
info_value(Clause, Pxs, Nxs, Value) :- 
 tuples(Clause, Pxs, Ptuples), 
 length(Ptuples, P), 
 ( P =:= 0 -> 
       Value = 0 
 ; tuples(Clause, Nxs, Ntuples), 
   length(Ntuples, N), 
   Temp is P / (P + N), 
   log(Temp, Temp1), 
   Value is Temp1 * -1.442695 
 ). 
 
 
% Determines the clause which is an extension of Clause by a single 
% literal and provides maximum information gain over the original 
% clause. 
best_next_clause([], _, _, _, _, _, Clause, Clause). 
best_next_clause([L|Ls], Nxs, Pxs, Clause, Info, Gain0, Best0, Best) :- 
 add_literal(L, Clause, Best1), 
 compute_gain(Nxs, Pxs, Info, Best1, Gain1), 
%% TH: For debugging purposes 
% \+ \+ ( numbervars(Best1,0,_), 
%  write('Gain: '), write(Gain1), write(' Clause: '), 
%  print(Best1), nl ), 
 ( Gain1 > Gain0 -> 
       best_next_clause(Ls, Nxs, Pxs, Clause, Info, Gain1, Best1, Best) 
 ; Gain1 =:= Gain0 -> 
       choose_tie_clause(Best0, Best1, Best2), 
       best_next_clause(Ls, Nxs, Pxs, Clause, Info, Gain0, Best2, Best) 
 ; best_next_clause(Ls, Nxs, Pxs, Clause, Info, Gain0, Best0, Best) 
 ). 
 
 
% In the case of an information tie, the clause with the viewest 
% number of variables is choosen. If both have the same number of 
% variables this design causes problems ! 
choose_tie_clause((A1:-B1), (A2:-B2), C) :- 
 variables_in(B1, V1), 
 length(V1, N1), 
 variables_in(B2, V2), 
 length(V2, N2), 
% TH: This was the initial formulation, which means: in case of a 
%     variable tie ignore the refinement and take the first clause. 
%     In this formulation neither the membertest example 'foil_3.pl' 
%     nor 'foil_4.pl' will be processed correctly ! 
% ( N2 < N1 -> 
%       C = (A2:-B2) 
% ;  C = (A1:-B1) 
% ). 
% TH: In this formulation, which means: in case of a variable tie use 
%     the refinement and ignore the previous possible clauses, 
%     the membertest example 'foil_4.pl' will be processed correctly, 
%     but 'foil_3.pl' will not terminate ! 
 ( N2 =< N1 -> 
       C = (A2:-B2) 
 ;  C = (A1:-B1) 
 ). 
% TH: Obviously, this implies that chosing arbitrarily a clause in the 
%     case of a variable tie is the wrong solution. It would be 
%     better to specialize those clauses further and to decide one 
%     step later, which branch to follow. Unfortunately, Quinlan 90 
%     seems to give no answer to this problem ! 
  
% For a set of positive and negative examples Pxs and Nxs, compute the 
% information gain of Clause over a clause which produces a split 
% having Info, as it's "information value" on these examples. 
compute_gain(Nxs, Pxs, Info, Clause, Gain) :- 
 covered_examples(Clause, Pxs, Retained), 
 length(Retained, R), 
 ( R =:= 0 -> 
       Gain = 0 
 ; info_value(Clause, Pxs, Nxs, Info1), 
   Gain is R * (Info - Info1) 
 ). 
  
% Add a literal to the right end of a clause 
add_literal(L, (A :- B), (A :- B1)) :- 
 ( B = true -> 
       B1 = L 
 ; B1 = (B,L) 
 ). 
 
 
add_literals(Ls, Clause0, Clause) :- 
 ( Ls = [] -> 
       Clause = Clause0 
 ; Ls = [L|Ls1], 
   add_literal(L, Clause0, Clause1), 
   add_literals(Ls1, Clause1, Clause) 
 ). 
  
% Construct a list representing the set of variables in Term. 
variables_in(A, Vs) :- 
 variables_in(A, [], Vs). 
  
variables_in(A, V0, V) :- 
 var(A), !, 
 ord_add_element(V0, A, V). 
variables_in(A, V0, V) :- 
 ground(A), !, V = V0. 
variables_in(Term, V0, V) :- 
 functor(Term, _, N), 
 variables_in_args(N, Term, V0, V). 
 
 
variables_in_args(N, Term, V0, V) :- 
 ( N =:= 0 -> 
       V = V0 
 ; arg(N, Term, Arg), 
   variables_in(Arg, V0, V1), 
   N1 is N-1, 
   variables_in_args(N1, Term, V1, V) 
 ). 
 
 
% Given a clause and a list of examples, construct the list of tuples 
% for the clause.  A tuple is the binding of values to variables such 
% that the clause can be used to prove the example. 
tuples((A :- B), Xs, Tuples) :- 
 variables_in((A :- B), Vars), 
 variables_in(A, HeadVars), 
 length(HeadVars, N1), 
 length(Vars, N2), 
 ( N1 =:= N2 -> 
       %% shortcut - only need 1 proof if no new variables. 
       findall(Vars, (member(A, Xs), \+(\+ B)), Tuples) 
 ; findall(Vars, (member(A,Xs), call(B)), Tuples) 
 ). 
 
 
% Xs1 are the examples from Xs that can be proved with the clause 
covered_examples((A :- B), Xs, Xs1) :- 
 findall(A, ( member(A,Xs), \+( \+ B ) ), Xs1). 
 
 
% Xs1 are the examples from Xs that cannot be proved with the clause. 
uncovered_examples((A:-B), Xs, Xs1) :- 
 findall(A, ( member(A, Xs), \+ B ), Xs1 ). 
 
 
% Generate possible literals, which can be used to extend the clause 
generate_possible_extensions((A :- B), Extensions) :- 
 variables_in((A :- B), OldVars), 
        %% TH: This differs from the original implementation, which 
 %%     was not correct, since findall usually loses the 
 %%     variable bindings. 
 findall((OldVars :- L), candidate_literal(A, OldVars, L), Extension1), 
 rmhead(Extension1,OldVars,Extensions). 
 
 
% Compute a candidate literal. If the switch foil_use_negations/1 is 
% set also negated literals are generated. 
candidate_literal(Goal, OldVars, Lit) :- 
 foil_predicates(Preds), 
 member(Pred/Arity, Preds), 
 functor(L, Pred, Arity), 
 recursion_check(Goal, Pred, Arity, RecursionFlag), 
 MaxNewVars is Arity - 1, 
 possible_new_vars(RecursionFlag, MaxNewVars, NewVars), 
 length(NewVars, NewVarPositions), 
 OldVarPositions is Arity - NewVarPositions, 
 list_of_n_from(OldVars, OldVarPositions, [], OldVarSeq), 
 recursion_safe(RecursionFlag, Goal, OldVarSeq), 
 possible_unification(NewVars, NewVarSeq, _), 
 subseq(VarSeq, OldVarSeq, NewVarSeq), 
 bind_vars(L, VarSeq, 1), 
 ( Lit = L 
 ; foil_use_negations(true), 
   Lit = (\+ L) 
 ). 
 
 
recursion_check(G, Pred, Arity, Flag) :- 
 ( functor(G, Pred, Arity) -> 
       Flag = true 
 ; Flag = false 
 ). 
 
 
possible_new_vars(true,_,[]). 
possible_new_vars(false, N, L) :- 
 length(L,N). 
possible_new_vars(false, N, L) :- 
 N > 0, 
 N1 is N - 1, 
 possible_new_vars(false, N1, L). 
 
 
list_of_n_from(Elements, N, List0, List) :- 
 ( N is 0 -> 
       List = List0 
 ; N1 is N - 1, 
   member(E, Elements), 
   list_of_n_from(Elements, N1, [E|List0], List) 
 ). 
 
 
recursion_safe(true, Goal, OldVarSeq) :- 
 !, 
 \+ (numbervars(Goal, 0, _), ground(OldVarSeq)). 
recursion_safe(false, _, _). 
 
 
possible_unification([], [], []). 
possible_unification([H|T], [H|Result], [H|Vars]) :- 
 possible_unification(T,Result,Vars). 
possible_unification([H|T], [H|T1], Vs) :- 
 possible_unification(T, T1, Vs), 
 member(V,Vs), 
 H = V. 
 
 
bind_vars(Lit, Vars, Index) :- 
 ( Vars = [] -> 
       true 
 ; Vars = [H|T], 
    arg(Index, Lit, H), 
   Index1 is Index + 1, 
   bind_vars(Lit, T, Index1) 
 ). 
 
 
rmhead([],_,[]). 
rmhead([(Vars :- B)|Rest],Vars,[B|Result]) :- 
 rmhead(Rest,Vars,Result). 
 
 
%--------------------------------------------------------------------------- 
% Closed World Assumption on the Herbrand base 
 
 
create_universe(Universe) :- 
 setof(Term, term_of_ext_def(Term), Universe). 
 
 
term_of_ext_def(Term) :- 
 foil_predicates(PredSpecs), 
 member(Pred/Arity, PredSpecs), 
 functor(Goal, Pred, Arity), 
 call(Goal), 
 between(1, Arity, ArgPos), 
 arg(ArgPos, Goal, Term). 
 
 
create_negatives([P|Ps], Negatives) :- 
 functor(P, F, N), 
 functor(Template, F, N), 
 create_universe(Universe), 
 setof(Template, 
       (  arguments_are_members(Template, N, Universe), 
          \+ member(Template, [P|Ps]) ), 
      Negatives). 
  
arguments_are_members(Term, N, Universe) :- 
 ( N > 0 -> 
       arg(N, Term, Arg), 
       member(Arg, Universe), 
       N1 is N-1, 
       arguments_are_members(Term, N1, Universe) 
 ; true 
 ). 
  
%--------------------------------------------------------------------------- 
% Determinate Literals 
 
 
% determinate(+Lit, +Vars, +PTuples, +NTuples) -- holds if Lit is a 
% determinate literal wrt the bindings for Vars as represented in 
% PTuples and NTuples. 
determinate(L, Vars, PTuples, NTuples) :- 
 binds_new_var(L, Vars), 
 determ_cover(PTuples, L, Vars), 
 determ_partial_cover(NTuples, L, Vars). 
 
 
binds_new_var((\+ _),_) :- 
 !, fail. 
binds_new_var(L, Vars) :- 
 variables_in(L, LVars), 
 member(V,LVars), 
 \+ contains_var(V, Vars), 
 !. 
 
 
determ_cover([], _, _). 
determ_cover([T|Ts], Lit, Vars) :- 
 findall(Lit, (Vars = T, call(Lit)), [_]), 
 determ_cover(Ts, Lit, Vars). 
 
 
determ_partial_cover([], _, _). 
determ_partial_cover([T|Ts], Lit, Vars) :- 
 findall(Lit, (Vars=T, call(Lit)), Xs), 
 (Xs = [] ; Xs = [_]), 
 determ_partial_cover(Ts, Lit, Vars). 
 
 
bounded_determinate_literals(0, _, _, _, _, []) :- !. 
bounded_determinate_literals(Bound, Cands, (A:-B), Pxs, Nxs, DLits) :- 
 determinate_literals(Cands, (A:-B), Pxs, Nxs, DLits0), 
 reachable_antes(Bound, A, DLits0, DLits). 
 
 
determinate_literals(Cands, Clause, Pxs, Nxs, DLits) :- 
 variables_in(Clause, Vars), 
 tuples(Clause, Pxs, PTuples), 
 tuples(Clause, Nxs, NTuples), 
 Clause = (_:-Body), 
 determinate_literals1(Cands, Body, Vars, PTuples, NTuples, DLits). 
 
 
determinate_literals1(Cands, Body, Vars, PTuples, NTuples, DLits) :- 
 bagof(X, ( member(X, Cands), 
            determinate(X, Vars, PTuples, NTuples), 
     \+( (numbervars(Vars,0,_), ante_memberchk(X,Body)) ) 
   ), 
       DLits). 
 
 
ante_memberchk(A,A) :- !. 
ante_memberchk(A, (B,C)) :- 
 ( ante_memberchk(A,B) -> 
       true 
 ; ante_memberchk(A,C) 
 ). 
 
 
% reachable_antes(+Bound, +H, +Cands, -Antes) -- Antes is the list of 
% literals from Cands which can be "connected" to H by some chain of 
% variables of length <= Bound. 
reachable_antes(Bound, H, Cands, Antes) :- 
 variables_in(H, Vs), 
 expand_by_var_chain(Bound, Cands, Vs, [], Antes). 
 
 
expand_by_var_chain(Bound, Cands, Vars, As0, As) :- 
 ( Bound =:= 0 -> 
       As = As0 
 ; partition_on_vars(Cands, Vars, Haves, Havenots), 
   ( Haves = [] -> 
  As = As0 
   ; append(As0, Haves, As1), 
     variables_in(As1, Vars1), 
     Bound1 is Bound - 1, 
     expand_by_var_chain(Bound1, Havenots, Vars1, As1, As) 
   ) 
 ). 
 
 
partition_on_vars([], _, [], []). 
partition_on_vars([C|Cs], Vars, Hs, Hnots) :- 
 ( member(V, Vars), contains_var(V, C) -> 
       Hs = [C|Hs1], 
       Hnots = Hnots1 
 ; Hs = Hs1, 
   Hnots = [C|Hnots1] 
 ), 
 partition_on_vars(Cs, Vars, Hs1, Hnots1). 
 
 
%   ord_add_element(+Set1, +Element, ?Set2) 
%   is the equivalent of add_element for ordered sets.  It should give 
%   exactly the same result as merge(Set1, [Element], Set2), but a bit 
%   faster, and certainly more clearly. 
 
 
ord_add_element([], Element, [Element]). 
ord_add_element([Head|Tail], Element, Set) :- 
 compare(Order, Head, Element), 
 ord_add_element(Order, Head, Tail, Element, Set). 
 
 
ord_add_element(<, Head, Tail, Element, [Head|Set]) :- 
 ord_add_element(Tail, Element, Set). 
ord_add_element(=, Head, Tail, _, [Head|Tail]). 
ord_add_element(>, Head, Tail, Element, [Element,Head|Tail]). 
 
 
%   contains_var(+Variable, +Term) 
%   is true when the given Term contains at least one sub-term which 
%   is identical to the given Variable.  We use '=='/2 to check for 
%   the variable (contains_term/2 uses '=') so it can be used to check 
%   for arbitrary terms, not just variables. 
contains_var(Variable, Term) :- 
 \+ free_of_var(Variable, Term). 
 
 
%   free_of_var(+Variable, +Term) 
%   is true when the given Term contains no sub-term identical to the 
%   given Variable (which may actually be any term, not just a var). 
%   For variables, this is precisely the "occurs check" which is 
%   needed for sound unification. 
free_of_var(Variable, Term) :- 
 Term == Variable, 
 !, 
 fail. 
free_of_var(Variable, Term) :- 
 compound(Term), 
 !, 
 functor(Term, _, Arity), 
 free_of_var(Arity, Term, Variable). 
free_of_var(_, _). 
 
 
free_of_var(1, Term, Variable) :- !, 
 arg(1, Term, Argument), 
 free_of_var(Variable, Argument). 
free_of_var(N, Term, Variable) :- 
 arg(N, Term, Argument), 
 free_of_var(Variable, Argument), 
 M is N - 1, !, 
 free_of_var(M, Term, Variable). 
 
 
%   subseq(Sequence, SubSequence, Complement) 
%   is true when SubSequence and Complement are both subsequences of 
%   the list Sequence (the order of corresponding elements being 
%   preserved) and every element of Sequence which is not in 
%   SubSequence is in the Complement and vice versa.  That is, 
%   length(Sequence) = length(SubSequence)+length(Complement), e.g. 
%   subseq([1,2,3,4], [1,3,4], [2]).  This was written to generate 
%   subsets and their complements together, but can also be used to 
%   interleave two lists in all possible ways.  Note that if S1 is a 
%   subset of S2, it will be generated *before S2 as a SubSequence and 
%   *after it as a Complement. 
subseq([], [], []). 
subseq([Head|Tail], Sbsq, [Head|Cmpl]) :- 
 subseq(Tail, Sbsq, Cmpl). 
subseq([Head|Tail], [Head|Sbsq], Cmpl) :- 
 subseq(Tail, Sbsq, Cmpl). 
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% compound(X) :- \+ atomic(X), \+ var(X).

% Math code

% log(X,Y): Y is the natural logarithm (base e) of X.

log(0,0).

log(X,Y) :-
  X > 0,
  log_e_series(X,1,Y,1,99).


% log_e_series(X,Term,Y,Exp,Limit): Y is the natural logarithm (base e)
%   of X (X >= 0) according to the logarithmic series:
%
%   log_e (X) = 2 [ Term + (1/3)*Term^3 + (1/5)*Term^5 + ... +
%                          (1/Exp)*Term^Exp ]
%
%      where Term = ((X-1)/(X+1)) and Exp is the largest odd <= Limit.

log_e_series(_,_,0,Exp,Limit) :-
  Exp > Limit.

log_e_series(X,_,Y,1,Limit) :-
  Limit >= 1,
  Term1 is ((X-1)/(X+1)),
  Term2 is Term1 * 2,
  log_e_series(X,Term1,Y2,3,Limit),
  Y is Term2 + Y2.

log_e_series(X,Term,Y,Exp,Limit) :-
  Exp =< Limit,
  Exp > 1,
  Term1 is Term * ((X-1)/(X+1)) * ((X-1)/(X+1)),
  Term2 is Term1 * (2 / Exp),
  Exp2 is Exp + 2,
  log_e_series(X,Term1,Y2,Exp2,Limit),
  Y is Term2 + Y2.
 
