**************************************************************************************
**************************************************************************************
*
* M I L E S
*
* Modular Inductive Logic programming Experimentation System
*
* Overview of modules and exported predicates
*
**************************************************************************************
**************************************************************************************
**************************************************************************************
*******************MODULE argument_types**********************************************
**************************************************************************************
- argument_types:
toplevel predicate for determining argument types
results for each predicate p within the pos examples in a kb entry
type_restriction(p(V1,..,Vn),[type1(V1),...,typen(Vn)])
- type_equal(+Type_name1,+Type_name2):
Tests whether the types Type_name1 and Type_name2 are defined identically
(up to different type names)
- type_sub(+Gen,+Spec):
Gen, Spec: type names or intermediate type definitions t_int(H):- B (cf. type_of).
succeeds if the type Gen is more general than the type Spec.
- type_of(+Var,+C,-Type):
Returns the most specific type of Var within clause C.
If Var does not occur in C or if it occurs at positions with incompatible
types, type_of returns fail. If Var is a term that only partially matches
the body of a type definition, a intermediate type definition
t_int(Var):- B is returned
- types_of(+Varlist,+C,-Typelist):
like type_of for each Var in Varlist.
Varlist = [V1,..,Vn] => Typelist = [V1:T1,..,Vn:Tn]
- compare_types(+Type1,+Type2,-Type):
Type1,Type2: types to be compared
Type: the most specific type among type1 and typ2
- define_type: allows to define a type restriction for a predicate
- verify_types: checks for the type restrictions in the kb whether
they contain only defined or built-in types. If not,
the user is asked for replacing or defining the unknown types.
**************************************************************************************
**********************MODULE bu_basics************************************************
**************************************************************************************
- process_new_literals(+[H:Proof|_],-Flag):
H = Lit/M where M is in {new_head,new_body}, or H = []
Proof = [[Lit,N],..,[],...] where N in {head,body}
asserts all new heads and bodies of matched clauses via head/3 and body/3
Flag = 1 if at least one existed
- abs_process_proofs(+Proofs,-Head):
Proofs = [CL1,..,CLn] where CLi is a clause in list notation
Head: a head literal
returns a head literal from one of the CLi, and retracts
the according body literals body(L,_,_) of CLi (destructive absorption)
- ident_process_proofs(+[[H:Proof]|_],-Head):
H = Lit/M where M is in {new_head,new_body}, or H = []
Proof = [[Lit,N],..,[],...] where N in {head,body}
Head: a literal
returns a head literal from one of the H:Proof, and retracts the according literals
from Proof from the kb
- g1_process_proofs(+[[H:Proof]|_],-Lit):
H = Lit/M where M is in {new_head,new_body}, or H = []
Proof = [[Lit,N],..,[],...] where N in {head,body}
Lit: a literal and its sign
returns the resolution literal from one of the H:Proof, and retracts
the according literals from Proof from the kb
- assert_assorptions(+[CL|_],-Flag):
CL: clause in list notation
asserts heads H of all absorbed clauses, if new, as body(H,_,_). Flag=1 if at
least one existed
- annotate_redundancy(+Proof):
Proof: clause in list notation
increments counter for each body literal in Proof
- assert_body_randomly(+Clause_list):
+Clause_list ... Clause in list notation
assert body literals in random order
- addtolist(+ToAdd):
ToAdd .. Id or list of Id''s
asserts list of Id''s
- getlist(-ID_list):
retracts the list of id''s that has been asserted by addtolist/1
- cover_assert_assumptions(+Clause_list):
Clause_list .. clause in list representation
asserts for each literal L in Clause_list assumption(L,_,_) in the kb
- clear_mngr:
retracts all head/3 and body/3 within the knowledge base
- retract_body_literals(+CL):
CL: clause in list notation
retracts body(L,_,_) for each L:_ in CL
- retract_literals(+[[Lit,N]|_]):
N in {head,body}
retracts head(Lit,_,_)/body(Lit,_,_) for each [Lit,head]/ [Lit,body] in the input
- assert_literals(+[[Lit,N]|_]):
N in {head,body}
asserts each Lit with [Lit,N] in the input as N(Lit,_,_)
- assert_clause(+CL):
CL .. clause in list representation
asserts positive literals L in CL as head(L,old,0),
negative and redundant literals as body(L,old,0).
- assert_body(+CL):
CL ... clause body in list representation (only negative and redundant literals)
asserts each literal L in CL as body(L,old,0)
- assert_body_unique(+CL)
CL ... clause body in list representation (only negative and redundant literals)
as assert_body/1, but tests whether body(L,_,_) is already in the kb
- reset_counts:
for each kb-entry head(Lit,_,Count) and body(Lit,_,Count), Count is set to 0
- subs_build_clause(-CL):
CL ... Horn clause in list representation
retracts one entry head(H,_,_) and all entries body(L,_,_) and builds clause
[H:p,..,L:p,...]
- sat_build_clause(+H,+B,-CL):
H ... head
B ... list of body literals
CL ... Horn clause in list representation
build clause CL = [H:p,...,L:M,....] for each L in B, M is n, if body(L,_,_) is
true, else M is r
- msg_build_long_clause(-CL):
CL ... a general clause in list representation
- msg_build_heads(-CL):
CL ... clause in list representation, consisting only of positive literals
collects all Literals L such that head(L,_,_) is in kb, and returns
CL = [...,L:p,....]
- msg_build_body(-CL):
CL ... clause in list representation, consisting only of negative and
redundant literals
collects all Literals L such that body(L,_,_) is in kb, and returns
CL = [...,L:M,....], M in {n,r}
- idev_build_clause1(-CL):
CL .. Horn clause in list representation
- idev_build_body(-CL):
CL ... clause in list represenation, only negative and redundant literals
collects all L such that body(L,_,_) is in kb
- idev_build_clause(+H,-CL):
CL .. clause in list representation
H ... preferred head of CL
as idev_build_clause1/1, but with preferred head in CL
- idev_build_head(+PrefH,-H):
PrefH, H .. clause heads
returns H such that head(H,_,_) in kb and PrefH and H
unifiable. If none exists, the first H with head(H,_,_) in kb is returned.
- ident_build_body(-CL):
CL ... clause in list notation, contains only negative literals
CL = [...,L:n,...] for each L such that body(L,_,0) in kb
- g1_build_clause(+ResLit,-CL):
CL ... Horn clause in list notation
ResLit ... the resolution literal
CL is the second parent clause for the g1-operator
- abs_build_body(-CL):
CL .. clause in list representation, contains only negative literals
CL = [...,L:n,....] for each L such that body(L,_,_) in kb
**************************************************************************************
************************MODULE clause_heads*******************************************
**************************************************************************************
- clause_heads:
algorithm for determining clause heads covering all positive examples in
the kb; generates database entrys of the form known(ID,Head,true,CList,head,_)
- heads(-HL):
returns list of heads covering all positive examples in the kb
- heads(+Pred,+Arity)
determines clause heads covering all positive examples for Pred/Arity and asserts
them in the kb
- heads(+Pred,+Arity,-HL)
returns list of heads covering all positive examples for Pred/Arity
**************************************************************************************
************************MODULE div_utils**********************************************
**************************************************************************************
- remove(+I,+L,-L):
I .. number, L ... list of numbers
removes I from L (I occurs at most once in L)
- sort_by_length(+L,+Accu,-Accu):
L ... list of lists
Accu ... L sorted increasingly according to the length of sublists
sorts a list of lists increasingly according to the length of sublists
- mysetof(+Template,+Generator,-Set):
as setof/3, but succeeds with Set = [], if Generator fails
- sum(+LN,-S):
LN .. list of numbers, S number
if LN = [I1,..,In], then S = I1 + ... + In
- efface(+E,+L,-L):
E .. element of list L
removes the first element of L that is unifiable with E from L.
- effaceall(+E,+L,-L):
E .. element of list L
as efface, but allows backtracking
- best(+List,-Elem):
returns the first element of List, on backtracking the second etc.
- buildpar2(+Lit:M,+CL,-CL1):
Lit .. literal, M in {p,n,r}, CL and CL1 clauses in list representation
if M = p then CL1 = [Lit:p|CL] else CL1 results from CL by adding Lit:M at the end
- neg(+Lit:M,-Lit:M1):
Lit .... literal, M in {p,n,r}
switches the mark of the literal, i.e. if M = p then M1 = n and vice versa
- contains_duplicates(+L):
succeeds if L contains two unifiable elements
- identical_member(+Elem,+List):
succeeds if Elem is identically (==) contained in List
- convert_to_horn_clause(+PHead,+CL,-HCL)
PHead ... preferred head
CL ... general clause in list representation
HCL ... horn clause in list representation
if CL = [H1:p,..,Hn:p,L1:M1,..,Lm:Mm] where Mi in {p,r}
then HCL = [Hj:p,L1:M1,...,Lm:Mm], where Hj is the first
head in CL unifiable with PHead (if one exists), else the first head in CL
- extract_body(+CL,-CL1):
CL .. clause in list representation
CL1 = [...,L:M,...] where M in {p,n} and L in CL
- list_to_struct(+L,-C):
L ... list, C ... conjunction of elements of L
if L = [E1,...,En] then C = (E1,..,En)
- clist_to_prolog(+CL,-C)
CL .. Horn clause in list representation
C ... Horn clause in prolog format
convert list format to clause format and vice versa (should use body2list!!)
- append_all(+LL,-L):
LL .. list of lists, L .. list
appends all lists in LL -> L
- maximum(+L,-M):
L .. list of numbers, M number
M is the maximum element of L
- myforall(+E,+Pred):
E ... argument terms, Pred .. type predicate
calls Pred(e) for each e in E, and succeeds only if every call succeeds
- identical_make_unique(+L,-L1):
removes all identical duplicates (==) from L
- remove_v(+L0,+L,-L1):
removes each E in L0 from L if E is identically (==) contained in L
- make_unique(+L,-L1):
removes all duplicates (variant) from L
- variant_mem(+Elem,+List):
succeeds if an alphabetical variant of Elem is contained in List
- different_predicates(+L,-LL):
L .. list of terms, LL list of lists of terms
for each functor f/n occuring in L, LL contains a list Lf
consisting of all terms in L with principal functor f/n
- nth_arg(+E,+N,-Args):
E ... list of terms with principal functor p/n
N =< n argument position
Args ... list of argument terms
Args = {A | arg(N,P,A) and P in E}
- split_examples(+E,+Term,-P,-N):
P = {e in E | Term, e unifiable}
N = E - P
- shares_var(+T,+Ts):
T: a term or a clause,Ts: a list of terms or clauses
tests if T shares at least one variable with the terms in t
- body2list(?B,?BList):
B: Body of a clause (L1,...,Ln)
BList: [L1:x,...,Ln:x] where x is in {r,n}
transforms a clause body to a list of its literals
where each literal is augmented by :n (i.e. negative clause literal)
or :r (i.e. recursive goal in the clause body). works in both directions
- insert_unique(+N,+L,-L1):
N .. number, L,L1 sorted lists of numbers
inserts N uniquely in the ascendingly sorted list L
- insert_unique(+ID,+A,+L,-L1):
ID,A .. numbers, L,L1 = [...,ID:List,...]
inserts A in the sublist identified by ID in L
- genterm_test(+X/T,+Subst):
X/T element of a substitution, Subst substitution
succeeds if Subst contains a tuple Y/T1 such that T1 == T. In that case, X and Y
are unified.
- subset_chk(+L,+L1):
succeeds, if L is a subset of L1 (without unification)
- subterm_at_position(+Term,-Sub,+Pos,-Pos):
Term, Sub: Prolog terms
Pos: position of Sub within Term (a list of numbers)
returns a subterm of Term and its position, on backtracking further subterms
- part_of_clause(+Term,+Clause):
Term: a prolog term, Clause: a prolog clause
succeeds if Term is a literal within clause, a part of the clause body or the
clause itself
**************************************************************************************
************************MODULE environment********************************************
**************************************************************************************
- oracle( + Literal):
membership queries "Is the following literal always true?"
-> succeeds iff oracle answers yes
- oracle( + List_of_Clause_Ids, - Example_Id):
subset queries "Are the following clauses always true?"
If not, the user might supply a counter example.
Fails only if the oracle answers "no" AND does not supply a counter example
- oracle( + PnameAtom, - NewNameAtom):
name queries "How would you like to call predicate pXYZ", where pXYZ is a
new predicate. The oracle may use every atom as answer. However, the atom
"list" causes the system to show every known predicate symbol within
the knowledge base
The predicate returns the new predicate name, but does not replace the old
name by the new one within the kb.
- oracle(+Lit, -InstLit):
existential queries "Is there a correct instance of the following literal?"
If yes, the oracle supplies an instance -> InstLit. Else, the predicate fails
- oracle( + QuestionAtom, ? DefaultAtom, - AnswerAtom):
general questions with default answers. If no default is necessary,
use ''_'' as second argument
- satisfiable(+SG_list):
SG_list ... list of subgoals [...,[ID,Subgoal,Proof],...]
each Subgoal in SG_list is tested on satisfiability. The oracle is used
if the satisfiability of Subgoal can not be decided on the available knowledge
- ask_for(+Goal):
succeds if the ground atom Goal is valid in the kb, or declared to be
valid by the oracle
- confirm(+Clause_IDs,+Oldterm):
Clause_IDs .. list of clauseIDs,
Oldterm.. term of the predicate to be replaced
confirm new clauses and rename the new predicate (using the oracle)
if oracle refuses the new clauses, delete them; if they are accepted,
delete the old ones (see g2_op).
- get_ci(+L,-L)
reads the IDs of the Ci used for the g2-operator one by one
**************************************************************************************
**********************MODULE evaluation***********************************************
**************************************************************************************
- covered_examples(-CE):
returns IDs of all covered positive examples
- complexity(+ClauseID,-Size):
for kb references:complexity/2 calculates the size of a clause,
defined to be the number of constant and function symbol occurences
in the literals of the clause.
- complexity(+CL,-Size):
for clauses in list representation
- complexity(List_of_ClauseIDs,-Size):
for a list of kb references
- complexity(+Term,-Size):
for arbitrary prolog terms ( but not integers)
- complexity(+usr,-Size):
for all clauses with label usr
- complexity(+examples,-Size):
for all examples
- eval_examples:
One should use this to compute the evaluation for kb clauses!
o asserts for each example ID prooftrees(ID,Mark,Proofs), where
Mark in {success,fail} and Proofs are the successful/failing
proofs accordingly
o determines the evaluation of each rule in the kb according to
the current examples
- eval_pos_examples ( - List_of_Exs ):
Evaluate (= try to prove) all positive examples, return a list of the
ones which *cannot* be proved (empty list if successful).
Output-argument looks like [exID1:Fact1, exID2:Fact2, ...].
!!!Procedure does not compute evaluation for clauses!!
- complete_chk:
fails if not all *positive* examples covered
Does not compute evaluation for clauses!!
- correct_chk:
fails when first *negative* example covered
Does not compute evaluation for clauses!!
- fp(-OR):
a kind of shapiro''s contradiction backtracing that aims to detect possibly
overgeneral clauses. As it does not use an oracle, all possibly overgeneral
clauses are considered and a minimal combination such that all negative
examples become uncovered is returned.
Allows backtracking to an alternative set of possibly overgeneral clauses
OR is a list [I:E,...], where I is the index of a possibly overgeneral clause
and E is the set of wrong (head-)instantiations of clause I that should be
excluded by specializing I. OR is a minimal selection of possibly overgeneral
clauses such that by specialising them all negative examples become uncovered.
On backtracking, the second selection is returned, and so on.
- fpo(-OR):
as fp/1, but uses oracle
Allows backtracking to an alternative set of possibly overgeneral clauses
- ip(-UA_List)
UA_List ... list of ground atoms
Shapiro''s algorithm for diagnosing finite failure ip in our framework. Returns
a set of ground atoms that has to be covered to make all uncovered positive
examples succeed. Allows backtracking on alternative sets of ground atoms
that make all examples succeed.
**************************************************************************************
*************************MODULE filter************************************************
**************************************************************************************
- connected_vars(+ClauseIn,-ClauseOut,-Connected,-Unconnected):
ClauseIn,ClauseOut: clauses in list notation
Connected,Unconnected: list of variables
returns connected & unconnected vars
A variable is connected ( to the head literal ) iff
- it appears in the head, or
- it appears in a literal with a connected variable
A literal is connected iff it''s vars are.
- is_connected(+Clause):
a clause is connected if every variable is connected to the head.
- is_flat(+Clause), is_unflat(Clause):
succeeds/fails if Clause contains no function symbols
- truncate(+Strategy,+ClauseIn,-ClauseOut):
Strategy: one of { r, unconnected, unconnecting,strongly_generative}
ClauseIn,ClauseOut: integers (kb references)
performs truncation operator on ClauseIn using Strategy
The list of possible strategies is to be completed.
- truncate_r(ClauseIn,ClauseOut), truncate_r(ID):
drop all literals with label '':r'', i.e. drop all literals that were used
in saturation.
- truncate_flat_r(ClauseIn,ClauseOut), truncate_flat_r(ID):
drop all true literals with label '':r'', i.e. drop all literals that were
used in saturation, but no literals with type information ( suffix ''_p'').
- truncate_unconnected(+ClauseIn, -ClauseOut):
truncate unconnected body literals (see above)
- truncate_unconnecting(ClauseIn,ClauseOut):
connectivity heuristics for truncation: Drop a body literal if all
other literals remain connected. We added another constraint: the resulting
clause must be weakly generative.
Do not confuse the connectivity with the connectedness heuristics !!
- truncate_strongly_generative(+ClauseIn,-ClauseOut):
drop one body literal from a strongly generative clause s.t. the resulting
clause is also strongly generative.
- truncate_neg_based(+ClauseID)
truncate as many literals as possible, s.t. the resulting clause covers no
negative examples. This only works on unflat clauses; i.e. it only accounts
for dropping condition.
- truncate_flat_neg_based(+ClauseID)
truncate as many literals as possible, s.t. the resulting clause covers no
negative examples. As initial condition, the kb must be unflat. The truncation is
done on the flattened clause, so that this accounts for the dropping rule &
inverse subst. On exiting, the kb is unflat.
- truncate_j(+ClauseID,J)
J : integer = number of allowed new variables per literal
truncate all literals containing more than J variables not appearing in the head
of kb clause ClauseID.
truncate_j is remotely related to Muggleton''s ij-determination. We take i = 1.
More importantly, we cannot tell in our system, if a literal is determinate or not,
since we have no model.
- truncate_facts(+ClauseID)
truncate all body literals unifying with a kb fact labeled ''usr''.
- is_weakly_generative(+Clause)
a clause is weakly generative if all vars of its head appear also in another
literal
- is_strongly_generative(+Clause)
a clause is strongly generative if every variable appears in at least 2 literals
- noduplicate_atoms(+Clause)
tests whether the prolog clauseClause contains duplicate literals
- noduplicate_atom(+P,+B)
P: literal
B: clause body
tests if P already occurs(==) in B
- select_var_sharing_lits(+List_of_Clauses,-List_of_Clauses)
removes all clauses from List_of_Clauses the last literal of which does not
share a variable with the rest of the clause -> to be used during td-refinement
(not to add unconnected body literals)
- already_in(+N,+P,+Y)
N: arity of a literal P
P: literal
Y: term
succeeds if Y is(==) already an argument of P
**************************************************************************************
***************************MODULE flatten*********************************************
**************************************************************************************
Rouveirol''s representation change to function free Horn clauses. Shared variables
are deteced. Following the later versions of flattening(''90,''91) identical terms are
only represented once thru a new body literal. The older version (1989) introduced
for each occurence of a term a unique new body literal.
In the process of flattening all literals that are introduced for functions end
with the suffix "_p". In return, when unflattening a clause it is assumed that every
predicate symbol ending in "_p" stems from a function. This assumption is made
because the names for functions and predicates need to be distinct.
DON''T FLATTEN ANY CLAUSE CONTAINING LITERALS ENDING IN "_p" !!!
- flatten_term(+Term, -Literals):
Term: term to be replace by a variable, e.g. [a,b]
Literals: list of literals to replace Term
- flatten_literal(+Lit,-Lit_list):
returns the list of literals Lit has to be replaced with
- flatten_clause(+ClauseIn,-ClauseOut)
works on clauses in prolog notation, i.e. ( head :- body ) or list notation,
i.e. [ head:p , b1:n, b2:n, ... ]
- unflatten_clause(+FlatClause,-UnFlatClause)
FlatClause : flattened clause (either in list or prolog notation)
UnFlatClause : unflattened clause
Algorithm for unflattening: (Rouveirol,91.p131)
for each flattened predicate f_p(t1,..,tn,X) in the body of clause C
substitute all occurences of X by the functional term f(t1,..tn)
& drop f_p(t1,...,tn,X)
**************************************************************************************
************************MODULE g1_ops*************************************************
**************************************************************************************
- apply_g1( + NewClauseId, - List_of_ResultIds ):
Implementation of Ruediger Wirth''s G1-operator for inverse resolution corresponding
to his 1989 PhD thesis.
One might want to use apply_g1/2 if a new clause of background
knowledge is added to the kb and the G1-operator is to be applied.
If there already is a suitable "V", it will be extended and the
lgg of two A''s will be built.
A
Bi / \ Bj
\ Ai Aj /
\ / \ /
Ci Cj
If a clause A can be built as lgg of Ai and Aj (extend_g1/2), Ai and Aj will
be deleted.
- g1_op ( +ResolventID, +Parent1ID, -Parent2ID ),
g1_op ( +ResolventID, +Parent1ID, -Parent2ID, + Label ):
given a resolvent and one parent clause, the second parent clause is constructed
- absorb(+ExID, ?Parent1ID, -NewID):
apply one absorption step on input clause ExID; if Parent1ID is given, it
is tried to perform the absorption step with it as known parent. The resulting
clause is stored under NewID
Otherwise absorption will be performed with the first applicable background clause.
It is made sure that no 2 literals of a parent clause abs_match the same
literal in the resolvent.
- identify(+ExID, ?Parent1ID, -NewID):
apply one identification step on input clause ExID; if Parent1ID is given, it is
tried to perform the identification step with it as known parent. The resulting
clause is stored under NewID
Otherwise identification will be performed with the first applicable background
clause. It is made sure that no 2 literals of a parent clause ident_match the
same literal in the resolvent.
- inv_derivate(+ExID,-NewID),
inv_derivate(+ExID,+PrefHead,-NewID):
Muggleton''s inverse linear derivation; But: while in intermediate stages
several head literals might appear simultanously, the result will always
be a Horn clause. As head literal we choose the latest one derived in
inv_derivate/2. inv_derivate/3 takes as additional argument a literal, which is
interpreted as a preferred head. If it is possible, inv_derivate/3 results
in a Horn clause where the head matches this literal. The operator is restricted
to finding clauses at most 100 inverse resolution steps away.
- most_spec_v(+ExID, ?PID, -NewID):
Apply one most-spec-v operation to example with parent PID;
If PID is not given, take the first applicable clause
of bg as parent.
The most specific v comprises the most specific absorption
and the most specific identification.
Since we always want Horn clauses as a result, this operator
does not implement the most specific identification as
described by Muggleton: Instead of adding a second head
literal to the old clause, we replace the original head.
I.e. our most specific identification operator is destructive.
The most specific absorption remains nondestructive
- saturate(+ExID, -NewID), saturate(+ExID,-NewID,+Bound):
apply elementary saturation w.r.t. background clauses. It is bounded by at most
100 iterations, if bound is not given. When checking the preconditions for
firing one absorption step, it is made sure that no 2 literals of a parent
clause subsume the same literal in the resolvent.
- elem_saturate( +ExID, ?PID, -NewID):
Add head of parent from bg to body of resolvent. The Operator is identical to
Muggleton''s most-specific-absorption. When checking the preconditions for
firing one absorption step, it is made sure that no 2 literals of a parent
clause subsume the same literal in the resolvent.
**************************************************************************************
*************************MODULE g2_ops************************************************
**************************************************************************************
- intra_construct1(+C1,+C2,-A,-B1,-B2),
intra_construct1(+C1,+C2,-A,-B1,-B2,PName),
intra_construct1(+C1,+C2,-A,-B1,-B2,PName,Bound):
C1,C2,A,B1,B2: references to clauses in kb
PName: atom - name of invented predicate
Bound: integer
intra-construction where C1,C2 are at bottom of W, A at the center top, B1,B2
at outside top positions. S1(A) in C1, S2(A) in C2; the substitutions
between Bi & Ci are empty. Uses an ITOU-like heursitics for determining relevant
variables for the new predicate.
Our intra-construction will only work, if the two input clauses require the
same number of arguments for the newly invented predicate. This restriction is
not part of the original definition of intra-construction, but its at least
a very useful heuristics.
- intra_construct2(+C1,+C2,-A,-B1,-B2),
intra_construct2(+C1,+C2,-A,-B1,-B2,PName),
intra_construct2(+C1,+C2,-A,-B1,-B2,PName,Bound):
Uses a CIGOL-like heursitics for determining relevant variables for the new
predicate
- g2_op ( + C1_ID, + C2_ID, - A_ID, - B1_ID, - B2_ID)
Implementation of Ruediger Wirth''s G2-operator for inverse resolution corresponding
to his 1989 PhD thesis.
We generalize the Ci using Plotkin''s LGG, then build a new predicate as resolution
literal, find the argument terms for the new predicate (in a heuristic manner) and
finally build the Bi using our G1-operator.
The compression achieved is evaluated thru a simple, though quite sophisticated
complexity heuristic. If the resulting clauses show some compression, the are passed
to the oracle for confirmation and the user gets a chance to rename the new predicate.
Clauses which become obsolete during the process will be deleted.
- apply_g2( + CC, - A, -BB):
tries to apply the G2-operator to a set of clauses Ci.
The output will be a kb reference of the common parent clause A and a list of id''s
for parent clauses Bi.
Bi A Bj
\ / \ /
\ / \ /
Ci Cj
- apply_g2( - A, -BB):
ORACLE is asked to enter the Id''s of resolvent clauses Ci one by one.
This continues until oracle says ''stop''. Doubles and answers which are not a number
are ignored. Finally apply_g2/3 is called.
- apply_g2 ( + C1_ID, + C2_ID, - A_ID, - B1_ID, - B2_ID):
simply calls g2_op/5
**************************************************************************************
*************************MODULE interpreter*******************************************
**************************************************************************************
- ip_part1(+Goal,-Proof):
Goal: an uncovered positive example
Proof: a failing proof for the positive example
works exactly as the general interpreter solve0/2. The only difference is that
instead of failing when a system goal is failing or a proof is looping or rules
are missing, the interpreter continues, assuming that the failing goals should
be correct
- ip_part2(+Proofs,+Goal,-Uncovered_Atoms):
Proofs: failing proofs determined by ip_part1,
Goal: uncovered positive example
Uncovered_Atoms: Atoms that make Goal succeed, if they were covered by the kb
the satisfiability of each subgoal within failing proof is determined. For that,
the oracle might be necessary.
- proof_path(+Ex,+Pred,+Type,-ClauseIDs):
Ex: example for p/n
Pred = p(X1,..,Xn): most general term of p/n
Type = typei(Xi) for an argument of p/n
ClauseIDs: list of clauseIDs that have beed used for proving
typei(ei) for the ith argument of Ex
simulates the proof of typei(ei) for the ith argument of Ex and collects the indices
of all used clauses
- t_interpreter(+Goal,+ClauseList):
Goal: goal type(Arg), Arg ground
ClauseList: List of clauses defining different types
proves type(Arg) from ClauseList as kb
- solve(+Goal,-Mark,-Proofs):
Goal: ground atom or rule with ground head
Mark: success or fail
Proofs: all succeeding/failing proofs according to Mark
format for Proofs: [P1,..,Pn]
where Pi = [ID,Head,PBody] where ID is the ID of the
applied rule (sys for system predicates, -1 if no rule
is applicable), Head is the instantiation of the rule head,
and PBody is the proof of the rule body. PBody is of the form
- [], if Head is true
- fail, if Head is a failing syspred
- looping if the proof is looping on Head
- no_rules if no rules match Head
- recursively of the form [B1,..,Bm]
- solve_once(+Goal,-Mark,-Proof):
as solve/3, but proves Goal only once
- prove1(+Clause, -Proof):
Clause: clause in list form ( [H:p,L1:n,L2:n,..])
Proof: list of all literals used to prove clause
prove1 tries to match Clause against literals in this kb, used for clause
reduction wrt theta-subsumption (Plotkin).
This is a more efficient version for embedding Clause in the kb: (IRENE)
a list CL1 = [Lit:Sign:Litlist|_] is constructed from Clause where Litlist is
the list of literals in the kb (if Sign = p, literals head(L,_,_), else body(L,_,_))
unifiable with Lit. CL1 is sorted ascendingly according to the length of Litlist.
If there is an empty Litlist in CL1, prove1a fails and backtracking occurs.
Else Lit is unified with a literal in Litlist (backtrack point), and the remaining
list CL1 is updated.
- prove3(+CL,-CL):
CL: clause body in list notation
embedd CL in skolemized body of an example clause (body/3 entries in the kb)
used for absorption, saturation
- prove4(+CL,-Uncovered,-Proof):
CL: clause in list notation
Uncovered = H/M, where M in {new_head,new_body}
or Uncovered = [] if all literals are covered
Proof = [[Lit,N],...] where N in {head,body}
embeds CL in skolemized example clause (head/3,body/3 entries)
allows 1 uncovered literal (= the resolution literal) & returns it
- prove5(+HS,+RuleIDs):
HS: skolemized clause head, RuleIDs: list of ruleIDs
tries to infer HS from assumptions and the rules in RuleIDs
**************************************************************************************
****************************MODULE kb*************************************************
**************************************************************************************
- gen_id(-New)
generates a new kb id
- init_kb (+Filename), init_kb (+Filename, +Label):
the file Filename may contain Horn clauses "H:-B." and "H.", examples
"ex(Fact,Class)" and comments "% blabla". Examples are stored in the kb
as "ex(ID, Fact, Class)", clauses as
"known(ID,Head,Body,Clist,Label,evaluation(1,2,3,4,5,6,7,8,9))".
where ID ... unique kb identifier (a natural number)
Class ... +,-,?
Clist ... clause in list representation
[head:p, body1:n, body2:n, body3:r, ...]. Each literal is
marked p(positiv), n(negativ) or r(negativ + redundant)
Label ... e.g. the generating operator
default used for init_kb/1: usr
evaluation ... of the clauses w.r.t. the examples:
1... #applications of the clause
2... #definitively positive examples covered by the clause
3... list of definitively positive examples covered by the clause
of the form [...exID:Fact........]
4... #definitively negative examples covered by the clause
5... list of definitively negative examples covered by the clause
of the form [...exID:Fact........]
6... #probably positive examples covered by the clause
i.e. instantiations of the clause used in successful
proofs of positive examples
7... list of probably positive examples covered by the clause
[...exID:Fact........] where exID is the example of which the
proof uses fact as subgoal
8... #probably negative examples covered by the clause
i.e. instantiations of the clause used in successful
proofs of negative examples
9... list of probably negative examples covered by the clause
[...exID:Fact........] where exID is the example of which the
proof uses fact as subgoal
For each example, all possible prooftrees are stored in the kb:
"prooftrees(ID,M,Trees)" where M is success or fail and Trees contains
all successful or failing proofs of example ID.
init_kb can be used successively for different files
- consult_kb(+ Filename):
Restore knowledge base from qof-file which was produced by save_kb/1.
- save_kb(+ Filename):
Save snapshot of current knowledge base as compiled file
- clear_kb:
deletes all rules and examples from the kb
- store_clause (?prolog-clause,?clause-list,+label,-ID):
Store new clause in knowledge base (provide either horn-clause
or clause-list), label it and receive the unique clause-ID.
If store_clause is called with ID instantiated, it will fail if ID is
already in use in the knowledge-base. If not, ID will be used.
- store_clauses(+List_of_Clauses,+Label):
List_of_Clauses ... list of prolog clauses
Same as store_clause/4 for a list of clauses
- store_ex(?fact,?classification,-ID):
Store new example in knowledge base and receive the unique identification number.
If it is called with ID already instantiated: see above.
- get_example (? ID, ? Example, ? Classification),
get_clause (? ID, ? Head, ? Body, ? Clist, ? Label),
get_fact (? ID, ? Fact, ? Clist, ? Label),
get_evaluation (+ ID, - Evaluation):
read example/clause/fact or clause evaluation from the kb
- delete_clause(+ ID) ,
delete_example(+ ID),
delete_all(+list_of_clauseIDs):
delete clause(s)/example(s) with identifier(s) ID(list_of_clauseIDs)
- interpretable_predicate(-Term):
Term .. prolog term with principal funtor P/N
succeeds if rules or examples for P/N are in the kb
- assertallz(+List):
asserts all elements of List at the end of the kb
- rename (+ ID_list,+ Old_name,+ New_name ):
rename every occurence of predicate ''Old_name'' to ''New_name'' in a set of clauses
given as a list of kb-references (Id-list). ''New_name'' should be atomic.
- random_ex(-ID):
chooses randomly an example from the kb
- two_random_ex(-ID1,-ID2):
chooses randomly two examples from the kb
- i_random_ex(+I,-ExIDs):
selects randomly I examples from the kb
- shortest_clause(-ID:C):
ID .. clauseID, C ... complexity of the corresponding clause
selects the shortest clause from the kb
- two_shortest_clauses(-ID1:CL1,-ID2:CL2):
selects two shortest clauses from kb
- shortest_ex(-ID:C):
selects the shortest example from kb
- two_shortest_ex(-ID1:C1,-ID2:C2):
selects two shortest example from kb
- shortest_uncovered_ex(-ExID):
selects the shortest example that is not covered by the kb
- shortest_uncovered_ex(+ExIds,-ExId):
selects the shortest example among ExIds
- two_shortest_uncovered_ex(-ExID1,-ExID2):
selects two shortest examples that are not covered by the kb
- all_shortest_ex(-ExIds):
selects all shortest examples from kb
- all_shortest_uncovered_ex(-ExIds):
selects all shortest uncovered examples from kb
- no_rules, no_pos_examples, no_neg_examples, no_examples:
tests kb on the different properties
- delete_covered_examples:
deletes examples explained by the kb
- flatten_rules:
flattens all rules in the kb
- flatten_kb:
flattens kb (rules and examples)
- unflatten_kb:
unflattens a flat kb
- get_predlist(-Predlist):
Predlist = [P:PVars|_]
selects all predicates with a type restriction from kb & adapts type restrictions
by transfomation in a list [X:Tx,...] of variables X and types Tx
**************************************************************************************
**************************MODULE lgg**************************************************
**************************************************************************************
- reduce_complete(+Clause,-ReducedClause):
reduce clause with no repect to background knowledge (Plotkin,1970)
i.e. reduction wrt theta subsumption. Works on clauses in list form.
- reduce_approx(+Clause,-ReducedClause):
as reduce_complete except that the number of single reduction steps is bound
Works on clauses in list form.
- covered_clause(+RULES, +ID):
RULES: list of kb references (integers)
ID: id of clause to be tested
Test, if a clause is a specialization of RULES.
- covered_clauses(+RULES,+ToTest,-Covered,-Uncovered):
RULES: list of kb references (integers)
ToTest: either label of kb entries (lgg, sat, ex ..) or a list of kb references
test if RULES explain all example clauses denoted by ToTest.
Or: RULES |= clauses(ToTest)
- gen_msg(+ID1,+ID2,-ID), gen_msg(+ID1,+ID2,-ID,+Bound):
Approximation of Buntine''s most specific generalization. We saturate the 2
input clauses & build the lgg over them. Our procedure differs from Buntine''s
in that saturation does not construct all generalizing clauses under generalized
subsumption: if some head literal entailed by the body contains
unbound variables, saturation adds it to the body as it is, whereas Buntine
instead adds all of its ground instances. No reduction yet.
- rllg(+ID1,+ID2,-ID), rllg(+ID1,+ID2,+PrefHead,-ID):
Plotkin''s relative leat general generalization. Implementation thru Muggleton''s
alg.: Construct 2 inverse linear derivations, then build lgg over them.
If PrefHead is given & it is possible to find a rllg who''s head matches PrefHead,
rllg will construct this clause. No reduction yet.
- subsumes_list(+General,+Specific):
checks for theta subsumption by list matching. No proofs, no substitutions
are returned. General will not be instantiated. Works on clauses in list form.
- lgg_terms( + Term1, + Term2, - GenTerm ),
lgg_terms( + Term1, + Term2, - GenTerm,
- Subst_Term1, - Subst_Term2 ),
lgg_terms( + Term1, + Term2, - GenTerm,
- Subst1, - Subst2,
+ Init_Subst1, + Init_Subst2 ):
Term1,Term2,GenTerm: prolog terms
Subst_termi: [Var/Fi,..] substitution such that Termi = GenTerm Subst_termi
Plotkins least general generalisation wrt theta-subsumption on terms
- set_lgg(+List_of_Terms,-GenTerm)
lgg of a list of terms
- headed_lgg(+ID1,+ID2,-IDG), headed_lgg(+ID1,_ID2,-IDG,?Label):
returns lgg of clauses ID1 ID2 in IDG, if both clauses have a compatible head
literal (i.e. same pred, same arity). Fails else. Default label is hlgg
- hnr_lgg(+ID1,+ID2,-IDG), hnr_lgg(+ID1,_ID2,-IDG,?Label):
same as headed_lgg, except that the resulting generalised clause is NOT reduced.
Default label is hnrlgg
- lgg(+ID1,+ID2,-IDG), lgg(+ID1,_ID2,-IDG,?Label):
returns lgg of clauses ID1 ID2 in IDG. If both clauses have no compatible head
literal, the head literal of IDG is set to ''true''. Default label is lgg
- nr_lgg(+ID1,+ID2,-IDG), nr_lgg(+ID1,_ID2,-IDG,?Label):
same as lgg, except that the resulting generalised clause is NOT reduced.
Default label is nrlgg
- build_lgg(+IDs,+IID,-GID,+Label):
returns in GID the ID of the lgg of all clauses in IDs. IID is the ID of the
intermediate result
- lgg(+CL1,+CL2,-CLG,-Subst1,-Subst2), nr_lgg(+CL1,+CL2,-CLG,-Subst1,-Subst2):
CL1,CL2,CLG: clauses in list notation
Substi: Substitutions such that CLG Substi \subseteq CLi
CLG is (non-reduced) lgg of clauses CL1 and CL2
- headed_lgg(+CL1,+CL2,-CLG,-Subst1,-Subst2), hnr_lgg(+CL1,+CL2,-CLG,-Subst1,-Subst2):
CL1,CL2,CLG: clauses in list notation
Substi: Substitutions such that CLG Substi \subseteq CLi
CLG is (non-reduced) headed lgg of clauses CL1 and CL2
- gti(+C1,+C2,-C), gti(+C1,+C2,-C,-S1,-S2):
C1,C2,C: clauses in list notation
S1,S2: substitutions [ V1/Term1 , .... ]
generalization thru intersection, least general intersection
- lgti(+C1,+C2,-C,-S1,-S2),lgti(+C1,+C2,-C,-S1,-S2,+Bound):
apply gti-operator Bound times ( default: Bound = 10 ).
Return the longest resulting clause & substitutions.
**************************************************************************************
***********************MODULE newpred*************************************************
**************************************************************************************
- specialize_with_newpred(+ID,-Newclause,-Pos,-Neg)
where ID .. Clause ID, Newclause.. specialized clause
Pos.. positive examples for the new predicate
Neg.. negative examples for the new predicate
Specializes an overgeneral clause with a new predicate.
Returns the smallest number of arguments for the new predicate
such that Pos and Neg are disjunct (i.e. the new predicate really
makes the clause correct).
This is an implementation of CHAM/DBC''s method for argument search.
**************************************************************************************
***********************MODULE show_utils**********************************************
**************************************************************************************
- show_kb:
displays all clauses in kb asserted by known
- show_ex:
displays all examples in kb
- show_clause(+ ID):
displays the clause stored with ID
- show_clauses(+List_of_clauseIDs):
displays each clause with ID in List_of_clauseIDs
- show_kb_part(+From,+To)
From: the min ID of KB entries to be shown
To: the max ID of KB entries to be shown
shows all clauses with From <= ID <= To
- show_names:
lists all predicate names available in the kb
- print_kb(+ File):
prints kb to a file
- show_kb_types: displays definitions of all types in the kb
- show_type_restrictions: displays all type restrictions in the kb
- show_heads, show_bodies:
displays all intermediate heads/bodies stored by absorption, saturation,... in
the kb
- pp_clause(+CL):
CL .. clause in list notation
displays clause in list notation
- write_list(+List)
displays copy of a list after instantiating all terms within the copy by $Var(N)
**************************************************************************************
***********************MODULE td_basic************************************************
**************************************************************************************
- append_body(+Clause,+Literal,-Clause1):
Clause,Clause1.. Prolog clauses
adds Literal to the end of the body of Clause
- distribute_vars(+PVars,+Terms,-DVars):
PVars = [X:Tx|R]: terms X with types Tx in the new literal P
Terms: all terms with their types in the clause C to be refined
DVars = [X:Vx,...]: for each X in PVars a list of all type-matching
variables Vx in Terms + an additional new variable
computes DVars
- vars_of_type(+Terms,+Ty,-R2):
Terms= [X:Tx|_]: terms X with types Tx in the clause C to be refined
Ty: type Ty of an argument of the new literal
R2: a list of all terms in C matching type Ty
adds a term X of Terms to R2 if type Ty subsumes type of X or vice versa
and one new term (last element in R2)
- enumerate_t(+DVars,+PL,-PL2):
DVars = [X:Vx,...]: all variables X in the new literal
with their type-matching variables in C
PL: initial predicate list
PL2: predicate list
computes predicates P where variables in Vx are unified to X in P
**************************************************************************************
***********************MODULE tdref_it************************************************
**************************************************************************************
top-down refinement operators for Horn clauses (work iteratively)
- refinement_unify_variables(+Clause,+Terms,-CL):
Clause ... the clause to be specialized
Terms ... the terms that shall be used in refinement of the form [T:Type,...]
CL .... list of specialisations of Clause
refines clause by unifying variables. Returns list of specialised clauses
- refinement_instantiate_variables(+Clause,+Terms,-CL):
Clause ... the clause to be specialized
Terms ... the terms that shall be used in refinement of the form [T:Type,...]
CL .... list of specialisations of Clause
refines clause by instantiating variables with terms. Returns list of specialised
clauses
- refinement_add_body_literal(+Clause,+Terms,-CL):
Clause ... the clause to be specialized
Terms ... the terms that shall be used in refinement of the form [T:Type,...]
CL .... list of specialisations of Clause
refines clause by adding a body literal. Returns list of specialised clauses
- refinement(+ID,-CL):
ID: ID of a clause to be refined
CL: a list with refinements of the clause with ID
shapiro''s general refinement operator for a clause with ID (all terms are eligible
for refinement):
if there are covered positive examples:
- prepare for refinement:
a list of all terms and subterms augmented by their types and a list of all
variables in the clause with types
- refine clause by
- unifying variables within the clause
- instantiating variables within the clause to terms
- adding body literals. Only literals sharing at least a
variable with clause ID are allowed.
**************************************************************************************
********************************MODULE var_utils**************************************
**************************************************************************************
- vars(+Term,-Vars):
Term: any prolog term
Vars: list of variables in Term
- clause_terms(+Clause,-Termlist):
returns list of all non-ground terms in Clause
- terms(+Term,+Accu,-Accu), terms(+Count,+Term,+Accu,-Accu):
returns all non-ground subterms within Term
- only_vars(+Term,-Varlist):
returns all variables within Term
- typed_only_vars1(+TypedTermlist,-TypedVarlist):
TypedTermlist: [T:typeT,...]
Vars: [Var:typeVar,...]
extracts each term T that is a variable from a list TypedTermlist of terms with
type definition typeT.
- replace_t(+CL,List_of_typenames,Typename_new,-CL1):
CL,CL1 .. lists of Horn clauses
replaces in CL each occurrence of a typename in List_of_typenames by Typename
- replace(+C1,+S1,-C2,-S2):
C1, C2: clauses in list notation
S1, S2: replacements [ X / Term, .. ]
If all X''s are variables, this is actually a substitution, but we also allow
other terms. C2 is a copy of C1 with S1 applied. S2 is a copy of S1.
- inv_replace(+C1,+S1,-C2,-S2):
C1, C2: clauses in list notation
S1, S2: replacements [ X / Term, .. ]
C2 is a copy of C1 with term of S1 replaced by ass. vars
S2 is a copy of S1,s.t. vars(S2) in vars(C2).
this is not the inverse operation for replacement : We don''t distinguish
between the places of terms.
- term_size(+Term,-Size)
the code is a debugged copy from the Quintus library ''termdepth''
term_size(+Term, ?Size) calculates the Size of a Term, defined to be the number
of constant and function symbol occurrences in it.
- contains_vars(+Term,+Terms):
Term: any prolog term
Vars: list of prolog terms (also variables)
succeeds if all terms in Terms occur in Term
- flagged_contains_vars(+Term,+Terms,-Flag):
Term: any prolog term, Flag in {true,false}
Vars: list of prolog terms (also variables)
returns true if all terms in Terms occur in Term, else false
- inverse_substitute(+ClauseIn,-ClauseOut):
clauses in list notation, i.e. [ head(A):p, b1(A):n, .. ]
replace one term in ClauseIn by a variable. Thru backtracking all solutions can
be obtained. Implementation: flatten Clause, truncate one literal, truncate
unconnected literals, unflatten Clause.
Since identical terms are represented only once in our flattening, we cannot tell
between different places the terms appear at.
- inverse_substitute1(+CL,-CL):
CL,CL1: clauses in list notation
this is an alternative approach without flattening, it replaces terms by variables.
- skolemize(+Term1,-Subst,-Term2):
Term1,Term2: arbiraty prolog terms
Subst : substitution [ V1/t1, V2/t2, .. ]
where Vi are variables, ti skolem atoms
skolemization is a special substitution: all variables of Term1 are substituted by
atoms. One keeps track of the substitution thru Subst.
- deskolemize(+Term1,+Subst,-Term2):
Term1,Term2: arbiraty prolog terms
Subst : substitution [ V1/t1, V2/t2, .. ]
where Vi are variables, ti skolem atoms
Deskolemization reverses skolemization, if the skolem substitution is given
as input.
- skolems(+Term,-Skolems):
Term: skolemized term, Skolems: all skolem atoms in Term
- relevant_vars2(+C1,+C2,+Gen,+S1,+S2,-RelVars):
C1,C2,Gen: clauses in list notation. C1,C2 at bottom of W.
S1,S2: substitutions [V1=T1, .. ].
RelVars: list of vars [ V1, V2, .. ]
determine relevant vars with CIGOL heuristics. A variable V in Gen is relevant
if one of the terms T1, T2 it is substituted by in S1, S2 contains a variable that
also appears elsewhere in S1 or S2.
- relevant_vars3(+C1,+C2,+Gen,+S1,+S2,-RelVars):
C1,C2,Gen: clauses in list notation
S1,S2: substititions
RelVars : set of relevant vars
Gen is a common generaliztion of C1,C2 , s.t. S1(Gen) is a subsetof C1, and
analogously for C2. A variable is relevant if it appears in both Gen and
( C1 - Gen ) or Gen and ( C2 - Gen ).
- findargs(+CL,+Accu,-Accu):
CL: clause in list notation, Accu: arguments of the literals in CL
find all arguments of the literals of a given clause
- buildrelterms(+CL1,+CL2,+Clgg,+Subst1,+Subst2,-TermList):
CL1, CL2, Clgg .. clauses in list representation
Subst1,Subst2 ... substitutions such that Clgg Subst1 = CL1 and Clgg Subst2 = CL2
TermList ... list of relevant terms for the new predicate
determines the relevant terms for the new predicate as described in R. Wirth''s 1989
PhD thesis
- exists_intersect(+L1,+L2,-L):
L1,L2,L: lists
if nonempty intersection exists, succeeds and returns intersection, fails else
- clean_subst(+CL,+Subst,-Subst)
CL: clause in list notation, Subst: a substitution [X/Term,...]
removes all X/T from Subst such that X does not occur in CL