P-Progol


P-Progol User Manual

For Version 2.7.5. Later versions have been superseeded by Aleph. See http://www.comlab.ox.ac.uk/oucl/groups/machlearn/Aleph/aleph_toc.html.

Introduction

This document provides reference information on P-Progol, an implementation that contains aspects of the Progol algorithm. It is not intended to be an introduction to Progol nor to Inductive Logic Programming (ILP). Note that P-Progol has been superseeded by by Aleph. See http://www.comlab.ox.ac.uk/oucl/groups/machlearn/Aleph/aleph_toc.html.


The Progol algorithm is described in detail in S.H. Muggleton (1995), Inverse Entailment and Progol, New Gen. Comput., 13:245-286, available at ftp://ftp.cs.york.ac.uk/pub/ML_GROUP/Papers/InvEnt.ps.gz. A good introduction to the theory, implementation and applications of ILP can be found in S.H. Muggleton and L. De Raedt (1994), Inductive Logic Programming: Theory and Methods, Jnl. Logic Programming, 19,20:629--679, available at ftp://ftp.cs.york.ac.uk/pub/ML_GROUP/Papers/lpj.ps.gz.

P-Progol is intended to be a prototype for exploring ideas. It commenced in 1993 as part of a fun project undertaken by Ashwin Srinivasan and Rui Camacho at Oxford University. The main purpose was to understand ideas of inverse entailment which eventually appeared in Steve Muggleton's paper, and was accompanied by (good-natured) bun-fights about the execution speeds of programs being written by Ashwin (who was writing P-Progol) and Rui (who was writing Indlog). The earliest P-Progol implementation dates from April, 1993. There are, currently, at least 3 implementations based on the Progol algorithm: CProgol (by S. Muggleton, written in C which contains its own Prolog interpreter), Indlog (by Rui Camacho, in Prolog requiring the Yap compiler) and P-Progol (by Ashwin Srinivasan, in Prolog largely developed with Yap). The main differences in implementation (other than language) are in the search technique used and degree of user-interaction allowed. See section Related versions and programs for more details on obtaining these programs and differences between them.

The basic P-Progol algorithm

During routine use, P-Progol follows a very simple procedure that can be described in 4 steps:

  1. Select example. Select an example to be generalised. If none exist, stop, otherwise proceed to the next step.
  2. Build most-specific-clause. Construct the most specific clause that entails the example selected, and is within language restrictions provided. This is usually a definite clause with many literals, and is called the "bottom clause." This step is sometimes called the "saturation" step.
  3. Search. Find a clause more general than the bottom clause. This is done by searching for some subset of the literals in the bottom clause that has the "best" score. Two points should be noted. First, confining the search to subsets of the bottom clause does not produce all the clauses more general than it, but is good enough for this thumbnail sketch. Second, the exact nature of the score of a clause is not really important here. This step is sometimes called the "reduction" step.
  4. Remove redundant. The clause with the best score is added to the current theory, and all examples made redundant are removed. This step is sometimes called the "cover removal" step. Note here that the best clause may make clauses other than the examples redundant. Again, this is ignored here. Return to Step 1.

P-Progol is an implementation based around these 4 steps. A more advanced use of P-Progol (see section Advanced use of P-Progol) allows alteration to each of these steps.

Getting started with P-Progol

Loading P-Progol

P-Progol code is contained in a single file, usually called `progolXXX.pl' (the XXX stands for the current version number, for example progol272.pl refers to Version 2.7.2). To load P-Progol, you will need to consult this file into your Prolog compiler, with sufficient stack and heap size (the more, the better!). Here is an example of loading P-Progol into the Yap compiler, with a stack size of 5000 K bytes and heap size of 20000 K bytes:

yap -s5000 -h20000

[ Restoring file startup ]
 
yes

   ?- [progol272]. 

P-Progol requires 3 files to construct theories. The most straightforward use of P-Progol would involve:

  1. Construct the 3 data files called `filestem.b, filestem.f, filestem.n'. See section Background knowledge file, section Positive examples file, and section Negative examples file.
  2. Read all data using the read_all(filestem) command. See section Read all input files.
  3. Construct a theory using the induce command See section Construct a theory.

Background knowledge file

All background knowledge for P-Progol is contained in a file with a .b extension. Background knowledge is in the form of Prolog clauses that encode information relevant to the domain. It can also contain any directives understood by the Prolog compiler being used (for example, :- consult(someotherfile).). This file also contains language and search restrictions for P-Progol. Most basic amongst refer to modes, types and determinations (see section Mode declarations, section Type specifications, and section Determinations).

Mode declarations

These declare the mode of call for predicates that can appear in any clause hypothesised by P-Progol. They take the form:


mode(RecallNumber,PredicateMode).

where RecallNumber bounds the non-determinacy of a form of predicate call, and PredicateMode specifies a legal form for calling a predicate.

RecallNumber can be either (a) a number specifying the number of successful calls to the predicate; or (b) * specifying that the predicate has bounded non-determinacy. It is usually easiest to specify RecallNumber as *.

PredicateMode is a template of the form:


p(ModeType, ModeType,...)

Here are some examples of how they appear in a file:

:- mode(1,mem(+number,+list)).
:- mode(1,dec(+integer,-integer)).
:- mode(1,mult(+integer,+integer,-integer)).
:- mode(1,plus(+integer,+integer,-integer)).
:- mode(1,(+integer)=(#integer)).
:- mode(*,has_car(+train,-car)).

Each ModeType is either (a) +T specifying that when a literal with predicate symbol p appears in a hypothesised clause, the corresponding argument should be an "input" variable of type T; (b) -T specifying that the argument is an "output" variable of type T; or (c) # specifying that it should be a constant of type T. With these directives P-Progol ensures that for any hypothesised clause of the form H:- B1, B2, ..., Bc:

  1. Input variables. Any input variable of type T in a body literal Bi appears as an output variable of type T in a body literal that appears before Bi, or appears as an input variable of type T in H.
  2. Output variables. Any output variable of type T in H appears as an output variable of type T in Bi.
  3. Constants. Any arguments denoted by #T in the modes have only ground terms of type T.

Type specifications

Types have to be specified for every argument of all predicates to be used in constructing a hypothesis. This specification is done within a mode(...,...) statement (see section Mode declarations). For P-Progol types are just names, and no type-checking is done. Variables of different types are treated distinctly, even if one is a sub-type of the other.

Determinations

Determination statements declare the predicated that can be used to construct a hypothesis. They take the form:

 
determination(TargetName/Arity,BackgroundName/Arity).
 

The first argument is the name and arity of the target predicate, that is, the predicate that will appear in the head of hypothesised clauses. The second argument is the name and arity of a predicate that can appear in the body of such clauses. Typically there will be many determination declarations for a target predicate, corresponding to the predicates thought to be relevant in constructing hypotheses. If no determinations are present P-Progol does not construct any clauses. Determinations are only allowed for 1 target predicate on any given run of P-Progol: if multiple target determinations occur, the first one is chosen.

Here are some examples of how they appear in a file:

:- determination(eastbound/1,has_car/2).
:- determination(mult/3,mult/3).
:- determination(p/1,'='/2).

Positive examples file

Positive examples of a concept to be learned with P-Progol are written in a file with a .f extension. The filestem should be the same as that used for the background knowledge. The positive examples are simply ground facts. Here are some examples of how they appear in a file:

eastbound(east1).
eastbound(east2).
eastbound(east3).

Code exists in Version 1.9 onwards for dealing with non-ground positive examples. However, this has never been tested rigorously.

Negative examples file

Negative examples of a concept to be learned with P-Progol are written in a file with a .n extension. The filestem should be the same as that used for the background knowledge. The negative examples are simply ground facts. Here are some examples of how they appear in a file:

eastbound(west1).
eastbound(west1).
eastbound(west1).

Non-ground constraints can be a more compact way of expressing negative information. Such constraints can be specified in the background knowledge file (see section User-defined constraints). P-Progol is capable of learning from positive examples only. This is done using a Bayesian evaluation function (see posonly in section Evaluation functions).

Read all input files

Once the `filestem.b, filestem.f' and `filestem.n' files are in place, they can be read in P-Progol with the command:


read_all(filestem).

This will usually produce a long list of current settings that looks like:

        version=2.7.2
        construct_bottom=saturation
        lazy_on_cost=false
        nodes=5000
        etc.

If the flag record is set (see section Setting P-Progol parameters) then these settings, along with the date and machine that is currently being used are written to the file pointed to by the flag recordfile (see section Setting P-Progol parameters). Note that writing the date and machine details are written by calls to the date and hostname commands. These may not be available on all platforms.

Construct a theory

The basic command for randomly selecting examples and constructing clauses is:


induce.

When issued P-Progol does the four steps described by the basic Progol algorithm (see section The basic P-Progol algorithm). The result is usually a trace that lists clauses searched along with their positive and negative example coverage, like:


eastbound(A) :-
   has_car(A,B).
[120/5]
eastbound(A) :-
   has_car(A,B), short(B).
[120/5]
eastbound(A) :-
   has_car(A,B), open_car(B).
[120/5]
eastbound(A) :-
   has_car(A,B), shape(B,rectangle).
[120/5]

and the final result that looks like:


[theory]
 
[Rule 1] [Pos cover = 120 Neg cover = 0]

eastbound(A) :-
       has_car(A,B), short(B), closed(B).

[pos-neg] [120]

induce also reports the performance on the training data as a confusion matrix that looks like:


[Training set performance]

           Actual
        +          -  
     + 120         0         120 
Pred 
     -  0          5          5
 
       120         5         125
 
Accuracy = 100%

Performance on a test data is also reported if values for the parameters test_pos and test_neg are set (see section Setting P-Progol parameters).

induce implements a simple greedy cover-set algorithm. P-Progol allows you to experiment with a number of other ways of searching for answers (see section Altering the search).

Save a theory

The final theory constructed by P-Progol can be saved in a file FileName using the command:


write_rules(FileName).

Evaluate a theory

Besides automatic performance reporting, the theory constructed by P-Progol can be evaluated on examples in any data file using the command:


test(File,Flag,Covered,Total)

File is the name of the data file containing the examples. Flag is one of show or noshow. The former shows examples covered or otherwise. Both File and Flag have to be provided. test/4 then returns the following numbers. Covered is the number of examples in the data file covered by current theory. Total is the total number of examples in the data file.

Advanced use of P-Progol

Advanced use of P-Progol allows modifications to each of the steps to the basic algorithm (see section The basic P-Progol algorithm):

  1. Select example. A sample of more than 1 example can be selected (see samplesize in section Setting P-Progol parameters). The best clause obtained from reducing each corresponding bottom clause is then added to the theory. Alternatively, no sampling need be performed, and every example can be saturated and reduced (see induce_max in section Altering the search).
  2. Build most-specific-clause. Bottom clauses may be constructed "lazily" or not at all (see construct_bottom in section Setting P-Progol parameters). Literals in the a bottom clause may be evaluated "lazily" (see lazy_evaluate in section Other commands). Individual bottom clauses can be constructed and examined (see sat in section Other commands).
  3. Search. The search for clauses can be altered and customised to try different search strategies, evaluation functions, and refinement operators (see section Altering the search). A bottom clause can be reduced repeatedly using different search constraints (see reduce in section Other commands).
  4. Remove redundant. Examples covered may be retained to give better estimates of clause scores (see induce_cover, induce_max in section Altering the search).

Setting P-Progol parameters

The set/2 predicate forms the basis for setting a number of parameter values for P-Progol. Parameters are set to values using:

              set(Parameter,Value)

The current value of a parameter is obtained using:

              setting(Parameter,Value)

A parameter can be un-set by using:

              noset(Parameter)

Meaningful set/2 statements for P-Progol are:

set(i,+V)
V is an integer (default 2). Set upper bound on layers of new variables.
set(clauselength,+V)
V is an integer (default 4). Set upper bound on number of literals in an acceptable clause.
set(nodes,+V)
V is an integer (default 5000). Set upper bound on the nodes to be explored when searching for an acceptable clause.
set(minpos,+V)
V is an integer (default 1). Set a lower bound on the number of positive examples to be covered by an acceptable clause.
set(minacc,+V)
V is an floating point number between 0 and 1 (default 1.0). Set a lower bound on the minimum accuracy of an acceptable clause. This only makes sense if noise is not set.
set(noise,+V)
V is an integer (default 0). Set an upper bound on the number of negative examples allowed to be covered by an acceptable clause. This only makes sense if minacc is not set.
set(m,+V)
V is a floating point number. Sets a value for "m-estimate" calculations. See section Evaluation functions.
set(caching,+V)
V is one of: true or false (default false). If true then clauses and coverage are cached for future use. Only clauses upto length set by cache_clauselength are stored in the cache.
set(cache_clauselength,+V)
V is an integer (default 3). Sets an upper bound on the length of clauses whose coverages are cached for future use.
set(explore,+V)
V is one of: true or false (default false). If true and the verbosity level is at least 2 then all clauses with the same score as the current best clause are reported with the statement "exploratory clause." If verbosity level is below 2, search continues but reporting is suppressed. All internal pruning is turned off (see section Built-in and user-defined pruning).
set(explore_tolerance,+V)
V is floating point number. All clauses within the specified tolerance of the best current best clause are reported. Only makes sense if explore is set to true
set(openlist,+V)
V is an integer or inf (default inf). Set an upper bound on the beam-width to be used in a greedy search.
set(best,+V)
V is a `clause label' obtained from an earlier run. This is a list containing at least the number of positives covered, the number of negatives covered, and the length of a clause found on a previous search. Useful when performing searches iteratively.
set(record,+V)
V is one of: true or false (default false). If true then trace of P-Progol execution is written to a file. The filename is given by recordfile.
set(recordfile,+V)
V is a Prolog atom. Sets the filename to write a trace of execution. Only makes sense if record is set to true.
set(lazy_negs,+V)
V is one of: true or false (default false). If true then theorem-proving on negative examples stops once bounds set by noise or minacc are violated.
set(samplesize,+V)
V is an integer (default 1). Sets number of examples selected randomly by the induce or induce_cover commands. The best clause from the sample is added to the theory. A value of 0 turns off random sampling, and the next uncovered example in the sequence is selected.
set(gsamplesize,+V)
V is an integer (default 100). The size of the randomly generated example set produced for learning from positive examples only. See section Altering the search.
set(condition,+V)
V is one of: true or false (default false). If true then randomly generated examples are obtained after conditioning the stochastic generator with the positive examples.
set(search,+V)
V is one of: bf, df, heuristic, ibs, or ils (default bf). Sets the search strategy. See section Altering the search.
set(evalfn,+V)
V is one of: coverage, compression, posonly, pbayes, laplace, auto_m, mestimate, or user (default coverage). Sets the evaluation function for a search. See section Altering the search.
set(refine,+V)
V is one of: user, auto, probabilistic or false (default false). Specifies the nature of the customised refinement operator. If false then standard operation results. If user then the user specifies a refinement operator with refine/2 statements. If auto then an automatic refine/2 definition is generated prior to search. This is useful if a bottom clause is either not constructed or is constructed lazily. No attempt is made to ensure any kind of optimality and the same clauses may result from several different refinement paths. The setting for probabilistic is experimental and should not be used until further notice. In all cases other than a setting of false the parameter refineop is also set to true. See section Altering the search.
set(construct_bottom,+V)
V is one of: saturation, reduction or false (default saturation). Specifies the stage at which the bottom clause is constructed. If reduction then it is constructed lazily during the search. This is useful if the bottom clause is too large to be constructed prior to search. This also sets the flag lazy_bottom to true. The user has to provide a refinement operator definition (using refine/2). If not, the refine parameter is set to auto. If false then no bottom clause is constructed. The user would normally provide a refinement operator definition in this case.
set(proof_strategy,+V)
V is one of: restricted_sld or sld (default restricted_sld). If restricted_sld, then examples covered are determined by forcing current hypothesised clause to be the first parent clause in a SLD resolution proof. If sld then this restriction is not enforced. The former strategy is efficient, but not refutation complete. It is sufficient if all that is needed is to determine how many examples are covered by the current clause, which is what is needed when P-Progol is used to construct a set of non-recursive clauses greedily (for example using the induce/0 command: see section Construct a theory).
set(stage,+V)
V is one of: saturation, reduction or command (default command). Sets the stage of current execution. This is normally not user-set, and decided internally.
set(depth,+V)
V is an integer (default 5). Sets an upper bound on the proof depth to which theorem-proving proceeds. Not implemented in the Sicstus version See section No Depth Bound in Sicstus Progol.
set(splitvars,+V)
V is one of: true or false (default false). If set to true before constructing a bottom clause, then variable co-references in the bottom clause are split apart by new variables. The new variables can occur at input or output positions of the head literal, and only at output positions in body literals. Equality literals between new and old variables are inserted into the bottom clause to maintain equivalence. It may also result in variable renamed versions of other literals being inserted into the bottom clause. All of this increases the search space considerably and can make the search explore redundant clauses. The current version also elects to perform variable splitting whilst constructing the bottom clause (in contrast to doing it dynamically whilst searching). This was to avoid unnecessary checks that could slow down the search when variable splitting was not required. This means the bottom clause can be extremely large, and the whole process is probably not very practical for large numbers of co-references. The procedure has not been rigourously tested to quantify this.
set(lazy_on_cost,+V)
V is one of: true or false (default false). Specifies if user-defined cost-statements require clause coverages to be evaluated. This is normally not user-set, and decided internally (except in the Sicstus version See section No Auto Set of lazy_on_cost in Sicstus Progol).
set(lazy_on_contradiction,+V)
V is one of: true or false (default false). Specifies if theorem-proving should proceed if a constraint is violated.
set(print,+V)
V is an integer (default 4). Sets an upper bound on the maximum number of literals displayed on any one line of the trace.
set(pretty_print,+V)
V is one of: true or false (default false). If true prints text associated with a literal (using the text command).
set(verbosity,+V)
V is an integer (default 1). Sets the level of verbosity. Also sets the parameter verbose to the same value. A value of 0 shows very little.
set(test_pos,+V)
V is the name of the file containing the positive examples for testing.
set(test_neg,+V)
V is the name of the file containing the negative examples for testing.
set(train_pos,-V)
V is the name of the file containing the positive examples for training. This is set internally after the read_all command.
set(train_neg,-V)
V is the name of the file containing the negative examples for training. This is set internally after the read_all command.
set(skolemvars,+V)
V is an integer (default 10000). Sets the counter for variables in non-ground positive examples. Each variable will be replaced by a skolem variable that has a unique number which is no smaller than V. This number has to be larger than the number of variables that would otherwise appear in a bottom clause.
set(version,-V)
V is the current version of P-Progol. This is set internally.
set(+P,+V)
Sets any user-defined parameter P to value V. This is particularly useful when attaching notes with particular experiments, as all settings can be written to a file (see record). For example, set(experiment,'Run 1 with background B0').

Altering the search

P-Progol allows the basic search strategy to be altered in a number of ways. Besides the induce command, there are two other commands that can be used to construct clauses. The command:

             induce_cover.

is very similar to induce. The only difference is that positive examples covered by a clause are not removed prior to seeding on a new (uncovered) example. After a search with induce_cover P-Progol only removes the the examples covered by the best clause are removed from a pool of seed examples only. After this, a new example or set of examples is chosen from the seeds left, and the process repeats. The theories returned by induce and induce_cover are dependent on the order in which positive examples are presented. The command:

             induce_max.

is not affected by this order, as it saturates and reduces every example. The search is made more efficient by remembering the coverage of the best clause obtained so far for each example being generalised. Both induce_cover and induce_max are slower than induce, and usually produce clauses with a great deal of overlap in coverage. A separate program will have to be used to find some subset of these clauses that minimises this overlap (see T-Reduce in section Related versions and programs).

Search with P-Progol is controlled by two parameters. One sets the search strategy (search) and the other sets the evaluation function (evalfn).

Search strategies

A search strategy is set using set(search,Strategy). The following search strategies are recognised by P-Progol:

bf
Enumerates shorter clauses before longer ones. At a given clauselength, clauses are re-ordered based on their evaluation.
df
Enumerates longer clauses before shorter ones. At a given clauselength, clauses are re-ordered based on their evaluation.
heuristic
Enumerates clauses in a best-first manner.
ibs
Performs an iterative beam search as described by Quinlan and Cameron-Jones, IJCAI-95. Limit set by value for nodes applies to any 1 iteration. This is experimental.
ils
An iterative bf search strategy that, starting from 1, progressively increases the upper-bound on the number of occurrences of a predicate symbol in any clause. Limit set by value for nodes applies to any 1 iteration. This language-based search was developed by Rui Camacho and is described in his PhD thesis.

Evaluation functions

An evaluation function is set using set(evalfn,Evalfn). The following clause evaluation functions are recognised by P-Progol:

coverage
Clause utility is P - N, where P, N are the positive and negative examples covered by the clause.
compression
Clause utility is P - N - L + 1, where P, N are the positive and negative examples covered by the clause, and L the number of literals in the clause.
posonly
Clause utility is calculated using the Bayesian score described in S. H. Muggleton, (1996), Learning from positive data, Proc. Sixth Intnl. Workshop on Inductive Logic Programming, LNAI 1314, 358-376, Springer-Verlag, Berlin.
laplace (laplace estimate)
Clause utility is (P+1)/(P+N+2) where P, N are the positive and negative examples covered by the clause.
pbayes
Clause utility is the pseudo-Bayes conditional probability of a clause described in J. Cussens (1993), Bayes and Pseudo-Bayes Estimates of Conditional Probability and their Reliability, ECML-93, Springer-Verlag, Berlin.
mestimate
Clause utility is its m estimate as described in S. Dzeroski and I. Bratko (1992), Handling Noise in Inductive Logic Programming, Proc. Second Intnl. Workshop on Inductive Logic Programming, ICOT-TM-1182, Inst. for New Gen Comput Technology, Japan. The value of m is set by set(m,M).
auto_m
Clause utility is the m estimate with the value of m automatically set to be the maximum likelihood estimate of the best value of m.
user
Clause utility is -C, where C is the value returned by a user-defined cost function. See section User-defined cost specification.

Built-in and user-defined pruning

Two sorts of pruning can be distinguished within P-Progol. Internal pruning refers to built-in pruning that performs admissible removal of clauses from a search. This is currently available for the following evaluation functions: coverage, compression, posonly, laplace, mestimate, auto_m. User-defined prune statements can be written to specify the conditions under which a user knows for certain that a clause (or its refinements) could not possibly be an acceptable hypothesis. Such clauses are pruned from the search. The "prune" definition is written in the background knowledge file (that has extension `.b'). The definition is distinguished by the fact that they are all rules of the form:


prune((ClauseHead:-ClauseBody)) :-
        Body.

The following example is from a pharmaceutical application that states that every extension of a clause representing a "pharmacophore" with six "pieces" is unacceptable, and that the search should be pruned at such a clause.

prune((Head:-Body)) :-
        violates_constraints(Body).
 
violates_constraints(Body) :-
        has_pieces(Body,Pieces),
        violates_constraints(Body,Pieces).
 
violates_constraints(Body,[_,_,_,_,_,_]).

has_pieces(...) :- 

The use of such pruning can greatly improve P-Progol's efficiency. They can be seen as a special case of providing distributional information about the hypothesis space.

User-defined cost specification

The use of a user-specified cost function is a fundamental construct in statistical decision theory, and provides a general method of scoring descriptions. P-Progol allows the specification of the cost of a clause. The cost statements are written in the background knowledge file (that has extension `.b'), and are distinguished by the fact that they are all rules of the form:

cost(Clause,ClauseLabel,Cost):-
        Body.

where ClauseLabel is the list [P,N,L] where P is the number of positive examples covered by the clause, N is the number of negative examples covered by the clause L is the number of literals in the clause.

It is usually not possible to devise automatically admissible pruning strategies for an arbitrary cost function. Thus, when using a user-defined cost measure, P-Progol places the burden of specifying a pruning strategy on the user.

User-defined constraints

P-Progol accepts integrity constraints that should not be violated by a hypothesis. These are written in the background knowledge file (that has extension `.b') and are similar to the integrity constraints in the ILP programs Clint and Claudien. The constraints are distinguished by the fact that they are all rules of the form:

false:-
         Body.

where Body is a set of literals that specify the condition(s) that should not be violated by a clause found by P-Progol. It is usual to use the hypothesis/3 (see section Other commands) command to obtain the clause currently being considered by P-Progol. The following example is from a pharmaceutical application that states that hypotheses are unacceptable if they have fewer than three "pieces" or which do not specify the distances between all pairs of pieces.

false:-
        hypothesis(Head,Body,_),
        has_pieces(Body,Pieces),
        length(Pieces,N),
        N =< 2.
false:-
        hypothesis(_,Body,_),
        has_pieces(Body,Pieces),
        incomplete_distances(Body,Pieces).

The use of constraints is another way for P-Progol to obtain interesting hypothesis without negative examples. Ordinarily, this will result in a single clause that classifies every example as positive. Such clauses can be precluded by constraints. Note also that an integrity constraint does not state that a refinement of a clause that violates one or more constraints will also be unacceptable.

Constraints have a different syntax in the Sicstus version of P-Progol See section How to Express Constraints in Sicstus Progol.

User-defined refinement

P-Progol allows a method of specifying the refinement operator to be used in a search. This is done using a Prolog definition for the predicate refine/2. The definition specifies the transitions in the refinement graph traversed in a search. The "refine" definition is written in the background knowledge file (that has extension ".b"). The definition is distinguished by the fact that they are all rules of the form:

refine(Clause1,Clause2):-
           Body.

This specifies that Clause1 is refined to Clause2. The definition can be nondeterministic, and the set of refinements for any one clause are obtained by repeated backtracking. For any refinement P-Progol ensures that Clause2 implies the current most specific clause. Clause2 can contain cuts ("!") in its body.

The following example is from a pharmaceutical application that states that searches for a "pharmacophore" that consists of 4 "pieces" (each piece is some functional group), and associated distances in 3-D space. Auxilliary definitions for predicates like member/2 and dist/5 are not shown. representing a "pharmacophore" with six "pieces" is unacceptable, and that the search should be pruned at such a clause.

refine(false,active(A)).

refine(active(A),Clause):-
        member(Pred1,[hacc(A,B),hdonor(A,B),zincsite(A,B)]),
        member(Pred2,[hacc(A,C),hdonor(A,C),zincsite(A,C)]),
        member(Pred3,[hacc(A,D),hdonor(A,D),zincsite(A,D)]),
        member(Pred4,[hacc(A,E),hdonor(A,E),zincsite(A,E)]),
        Clause = (active(A):-
                        Pred1,
                        Pred2,
                        dist(A,B,C,D1,E1),
                        Pred3,
                        dist(A,B,D,D2,E2),
                        dist(A,C,D,D3,E3),
                        Pred4,
                        dist(A,B,E,D4,E4),
                        dist(A,C,E,D5,E5),
                        dist(A,D,E,D6,E6)).

Other commands

There are a number of other useful commands in P-Progol. These are:

rdhyp
Read a hypothesised clause from the user.
addhyp
Add current hypothesised clause to theory. If a search is interrupted, then the current best hypothesis will be added to the theory.
covers
Show positive examples covered by hypothesised clause.
coversn
Show negative examples covered by hypothesised clause.
reduce
Run a search on the current bottom clause, which can be obtained with the sat/1 command.
man(-V)
V is of location of the on-line manual.
commutative(+V)
V is of the form N/A, where the atom N is the name of the predicate, and A its arity. Specifies that literals with symbol N/A are commutative.
symmetric(+V)
V is of the form N/A, where the atom N is the name of the predicate, and A its arity. Specifies that literals with symbol N/A are symmetric.
lazy_evaluate(+V)
V is of the form N/A, where the atom N is the name of the predicate, and A its arity. Specifies that outputs and constants for literals with symbol N/A are to be evaluated lazily during the search. This is particularly useful if the constants required cannot be obtained from the bottom clause constructed by using a single example. During the search, the literal is called with a list containing a pair of lists for each input argument representing `positive' and `negative' substitutions obtained for the input arguments of the literal. These substitutions are obtained by executing the partial clause without this literal on the positive and negative examples. The user needs to provide a definition capable of processing a call with a list of list-pairs in each argument, and how the outputs are to be computed from such information. For further details see A. Srinivasan and R. Camacho, Experiments in numerical reasoning with ILP, To appear: Jnl. Logic Programming.
positive_only(+V)
V is of the form N/A, where the atom N is the name of the predicate, and A its arity. States that only positive substitutions are required during lazy evaluation of literals with symbol N/A. This saves some theorem-proving effort.
check_implication(+V)
V is of the form N/A, where the atom N is the name of the predicate, and A its arity. Specifies that literals with symbol N/A should be checked for logical redundancy before being added to an existing clause in the search. This is slow, and not well tested.
sat(+V)
V is an integer. Builds the bottom clause for positive example number V. Positive examples are numbered from 1, and the numbering corresponds to the order of appearance in the `.f' file.
example_saturated(-V)
V is a positive example. This is the current example saturated.
show(+V)
V is an one of: modes, determinations, settings, sizes, bottom, hypothesis, theory, pos, neg, rand, imap, prior, or posterior. These show the following:
modes
Current mode declarations.
determinations
Current determination declarations.
settings
Current parameter settings.
sizes
Current sizes of positive and negative examples.
bottom
Current bottom clause.
hypothesis
Current hypothesised clause.
theory
Current theory constructed.
pos
Current positive examples.
neg
Current negative examples.
rand
Current randomly-generated examples (used when evalfn is posonly).
imap
Current implication map (used in conjunction with check_implication/1).
prior
Current prior on refinement operator (this is experimental).
posterior
Current posterior on refinement operator (this is experimental).
modeh(+Recall,+Mode)
Recall is one of: a positive integer or *. Mode is a mode template as in a mode/2 declaration. Declares a mode for the head of a hypothesised clause. Required when evalfn is posonly.
modeb(+Recall,+Mode)
Recall is one of: a positive integer or *. Mode is a mode template as in a mode/2 declaration. Declares a mode for a literal in the body of a hypothesised clause.
modes(?PSym,?Mode)
PSym is of the form N/A, where the atom N is the name of a predicate, and A its arity. Mode is a modeh or a modeb template corresponding to PSym
determinations(?PSym1,?PSym2)
PSym1 and PSym2 are of the form N/A, where the atom N is the name of a predicate, and A its arity. True if determination(PSym1,PSym2) has been declared in the background file.
text(+L,+T)
L is a literal that can appear in the head or body of a clause. T is a list of terms that contain the text to be printed in place of the literal. Variables in the list will be co-referenced to variables in the literal. For example, text(active(X),[X, 'is active']). Then the clause active(d1) will be written as d1 is active.
hypothesis(-Head,-Body,-Label)
Head is the head of the current hypothesised clause. Body is the body of the current hypothesised clause. Label is the list [P,N,L] where P is the positive examples covered by the hypothesised clause, N is the negative examples covered by the hypothesised clause, and L is the number of literals in the hypothesised clause,

Related versions and programs

Yap version of P-Progol

This is the original version of P-Progol and uses the Yap Prolog compiler. It is maintained by Ashwin Srinivasan at the University of Oxford, and can be found at http://www.comlab.ox.ac.uk/oucl/research/areas/machlearn/PProgol/pprogol.pl. If you obtain this version, please inform Ashwin Srinivasan ashwin@comlab.ox.ac.uk. This version is free for academic use (research and teaching). If you intend to use it for commercial purposes then please contact Ashwin Srinivasan ashwin@comlab.ox.ac.uk.

NB: Yap is available at http://www.ncc.up.pt/~vsc/Yap/. P-Progol requires Yap 4.1.15 or higher, compiled with the DEPTH_LIMIT flag set to 1 (that is, include -DDEPTH_LIMIT=1 in the compiler options).

Sicstus version of P-Progol

The Yap version P-Progol was ported to use the Sicstus Prolog compiler by James Cussens, jc@cs.york.ac.uk, at the University of York. There are some differences as a result of underlying differences in Yap and Sicstus. This conversion refers version 2.7.1.

Running Sicstus P-Progol

Let us assume that the Sicstus version of P-Progol has been saved as progol.pl. Unless you intend to alter P-Progol very frequently, it a good idea to fcompile progol.pl to avoid having to recompile progol.pl each time you use it. You need to consult in progol.pl before fcompiling so that the operators in Progol are recognised:

SICStus 3  #5: Fri Aug 14 18:19:52 BST 1998
| ?- [progol], fcompile(progol).

fcompiling will create a file progol.ql. Now you can load in P-Progol with load(progol). If you haven't previously fcompiled P-Progol use compile(progol).

How Sicstus Progol Compiles Examples

Progol explicitly indexes examples: if the first example in the `.f' file is eastbound(train1) this is asserted as example(1,pos,eastbound(train1)). It is crucial for speed that example/3 is a compiled predicate.

Since, unlike Yap, Sicstus does not allow incremental compilation, it is necessary for Sicstus Progol to read in the `.f' and `.n' files, construct the example/3 facts, (and some bookkeeping goals) save them to a file with a `.exs' extension, and then compile this file.

Once a `.exs' file has been created, you can fcompile it into a `.exs.ql' file. If such a file exists, Progol simply loads it, since indexing and compilation are already done.

So, if you type, say, read_all(foo). Sicstus P-Progol does the following

  1. If there is a file `foo.exs.ql' this is loaded else;
  2. If there is a file `foo.exs' this is compiled else;
  3. Sicstus P-Progol indexes all examples in the files `foo.f' and `foo.n' and saves the indexed examples in a single `foo.exs' file, together with some bookkeeping goals. `foo.exs' is then compiled.

Remove any old `.exs' or `.exs.ql' files if you change your `.f' or `.n' files.

How to Express Constraints in Sicstus Progol

Constraints are expressed using false/1 rather than false/0 since false/0 is a built-in. The argument to false/1 will be instantiated to the current clause. Your constraint does not have to use this instantiation, although typically it will:

false((_Head:-Body)) :-
        has_literal(Body,Lit,_),
        functor(Lit,gender,_).

No Depth Bound in Sicstus Progol

There is no depth checking in Sicstus Progol since, unlike Yap, this is not built in to the Sicstus compiler. Setting the depth parameter via :- set(depth,40). will simply be ignored.

Positive Only Learning in Sicstus Progol

Progol uses an SLP to generate a set of random examples which is used to prevent overgeneralisation when learning from positive examples only. In Sicstus Progol, it is necessary to declare as dynamic all type predicates and all predicates that they call. This is so clause/2 can be used to implement the SLP. The random sample is not compiled as in Yap Progol. Also, one can not use internal Progol predicates to generate the random sample, after the positive examples have been read in. (This is not something most people would want to do.)

No Auto Set of lazy_on_cost in Sicstus Progol

Yap Progol can use clause/2 to inspect even compiled predicates, (since source is used). Sicstus can't, so it can't inspect the user cost definitions to decide is laziness is warranted. So you have to set lazy_on_cost yourself if you want it.

SWI version of P-Progol

The Yap version of P-Progol was ported to use the SWI Prolog compiler by Stephen Moyle at the University of Oxford. Details of this are available from Stephen Moyle, smoyle@ermine.ox.ac.uk, or Ashwin Srinivasan.

CProgol

A version of the Progol algorithm in the C language has been developed independently by Stephen Muggleton, and is available via ftp from the University of York. CProgol is independent of any compiler, as it contains its own interpreter for Prolog. Details of this are available from Stephen Muggleton, stephen@cs.york.ac.uk. Some key differences to CProgol 4.2 are below:

  1. Files. All data for CProgol is in a single file with a `.pl' suffix.
  2. Examples. Negative examples for CProgol have to be preceded by a :-, and can be non-ground. P-Progol does not require a :- prefix, and negative examples are ground (non-ground negative information is specified as constraints.)
  3. Modes. CProgol allows function symbols to appear in the literal template used in mode declarations. P-Progol does not.
  4. Search. CProgol performs the equivalent of P-Progol searches specified by: induce using set(search,heuristic) and set(evalfn,compression) or set(evalfn,posonly). CProgol does not allow user-specified refinement operators or cost functions. There is no equivalent of induce_cover/0 or induce_max/0 commands.

Indlog

Indlog is another Progol-like algorithm has been implemented by Rui Camacho, at the University of Porto. It uses the Yap Prolog compiler. Details of this are available from Rui Camacho, rcamacho@fe.up.pt.

T-Reduce

T-Reduce is a companion program to P-Progol that can be used to process the clauses found by the commands induce_cover and induce_max. This finds a subset of these clauses that explain the examples adequately, and have lesser overlap in coverage. T-Reduce uses the Yap Prolog compiler. Details of this are available from Ashwin Srinivasan, ashwin@comlab.ox.ac.uk.

Reference Manual

Change logs

Changes in Version 2.7.5

Predicates used in P-Progol

To avoid name-clashes, users must avoid using the following predicate symbols as they are used within P-Progol (Version 2.7.5). Entries in this table may change with subsequent versions.

abandon_branch/2
add_backs/1
add_cache/3
add_eqs/4
add_eqs/5
add_equivalences/3
add_generator/2
add_hyp/1
add_hyp/4
add_ioc_links/4
add_lit/8
add_litinfo/6
add_new_lit/8
add_ovars/2
add_prune_cache/1
add_skolem_types/1
add_skolem_types/3
add_skolem_types1/2
add_skolem_types2/2
add_types/1
addhyp/0
app_lit/3
append/3
apply_equivs/6
assemble_label/4
best_hypothesis/3
binom/4
binom_lte/4
built_in_prune/1
calc_intersection/3
call_library_pred/6
check_auto_refine/0
check_cache/3
check_implication/1
check_parents/4
check_posonly/0
check_prune_defs/0
check_user_search/0
choose/3
clause_distribution/2
clause_ok/3
clause_to_list/2
clean_up/0
clean_up_reduce/0
clean_up_sat/0
clear_cache/0
clear_hyp/0
collect_args/2
collect_example_cache/1
commutative/1
complete_clause_label/4
compression_ok/2
concat/2
condition/1
condition_target/0
construct_call/4
construct_incall/4
construct_name/3
construct_prolog_name/2
continue_search/3
copy_args/3
copy_args/4
copy_consts/3
copy_var/3
cost_cover_required/0
covers/0
covers/1
coversn/0
coversn/1
dappend/3
declare_dynamic/1
delete/3
delete0/3
delete1/3
delete_all/3
delete_list/3
depth_bound_call/1
determination/2
do_precomputation/0
equal_set/2
estimate_error/6
estimate_error_rate/5
estimate_variants/2
eval_rule/2
evalfn/2
evalfn/3
evalfn_name/2
evaluate/6
example/3
example_saturated/1
examples/2
execute/1
execute_equality/1
expand/12
explore_eq/2
extend_clause/3
extract_count/3
extract_cover/2
extract_cover/3
extract_length/2
extract_neg/2
extract_pos/2
find_beta_prob/2
find_count/2
find_hashed_variants/3
find_lazy_left/4
find_max_values/3
find_max_width/3
find_posgain/2
fix_base/2
flatten/5
flatten_args/5
flatten_atom/10
flatten_eq/7
flatten_lit/8
flatten_lits/11
flatten_terms/2
gen_auto_refine/0
gen_layer/2
gen_lit/1
gen_lits/2
gen_refine_id/1
gen_sample/2
gen_var/1
get_args/4
get_argterms/4
get_atoms/5
get_atoms1/5
get_besthyp/0
get_c_links/4
get_cache_entry/3
get_clause/4
get_determs/2
get_eqs/6
get_equivs/2
get_flatatom/4
get_gain/16
get_gain1/15
get_gains/15
get_hyp/1
get_hyp_label/2
get_i_links/5
get_implied/0
get_implied/3
get_ivars/3
get_ivars1/2
get_marked/3
get_max_negs/3
get_modes/2
get_next_atom/1
get_nextbest/1
get_node/4
get_nsuccesses/2
get_o_links/5
get_ovars/3
get_ovars1/2
get_pclause/6
get_pclause1/6
get_performance/0
get_predecessors/3
get_predicates/3
get_progol_clause/2
get_progol_lit/2
get_progol_lit/3
get_progol_lits/2
get_psyms/2
get_random/2
get_refine_gain/12
get_refine_id/2
get_repeats/3
get_search_keys/3
get_search_settings/1
get_sibgain/18
get_sibgains/15
get_sibpncover/7
get_start_label/2
get_successes/2
get_type_name/2
get_unmarked/3
get_user_refinement/4
get_var_equivs/6
get_vars/3
get_vars_in_term/2
goals_to_clause/2
goals_to_list/2
gsample/2
has_hashed/4
has_hashed_loc/2
hash_term/2
hashed_combinations/2
hashed_variant/3
hashed_variants/3
hypothesis/3
in_path/1
inc_beta_count/2
inc_beta_counts/2
inc_count/1
index_clause/3
index_prove/6
index_prove/8
index_prove1/6
index_prove1/9
induce/0
induce_cover/0
induce_max/0
induce_max/1
induce_max1/1
insert_eqs/3
integrate_args/3
integrate_args/4
integrate_head_lit/1
integrate_term/2
integrate_term/3
integrate_terms/3
intersect1/4
intersects/2
interval_count/2
interval_intersection/3
interval_subsumes/2
interval_subtract/3
interval_to_list/2
intervals_intersection/3
intervals_intersects/2
intervals_intersects/3
intervals_intersects1/2
intervals_intersects1/3
intervals_to_list/2
is_symmetric/3
label_create/2
label_create/3
label_ncover/2
label_pcover/2
label_print/1
label_union/3
lang_ok/2
lang_ok1/2
lazy_evaluate/1
lazy_evaluate/6
lazy_evaluate1/7
lazy_evaluate_refinement/5
lazy_evaluate_refinement/6
lazy_index_prove/4
lazy_index_prove1/4
lazy_prove/4
lazy_prove_neg/9
lazy_prove_negs/3
legal_term/4
length_ok/6
list_profile/0
list_to_clause/2
list_to_goals/2
list_to_interval/4
list_to_intervals/2
list_to_intervals1/2
lit_redun/2
make_sname/2
man/1
mark_lit/6
mark_lits/3
mark_lits/7
match_body_modes/1
match_bot/3
match_bot_lit/2
match_bot_lits/3
match_lazy_bottom/2
match_lazy_bottom1/1
match_mode/2
maxcovers/1
maxcoversn/1
maxlength_neg_ok/4
member/2
member1/2
member2/2
merge_vlist/2
mincovers/1
mincoversn/1
modeb/2
modeh/2
next_node/2
nlits/2
noset/1
occurs1/4
occurs_in/2
p1_message/1
p_message/1
partition/4
pfac/4
pos_ok/6
positive_only/1
pp_dclause/1
pp_dclause/2
pp_dlist/1
pp_dlist/2
prefix_lits/3
print_eval/2
print_lit/6
print_litlist/4
print_lits/4
print_node_count/2
print_text/1
probabilistic_extend/3
probabilistic_extensions/2
process_determs/0
process_mode/1
process_modes/0
progol_get_hlit/2
progol_get_lit/2
progol_has_ovar/3
progol_has_ovar1/4
progol_help/0
progol_help/1
progol_manual/1
progol_portray/1
progol_portray/2
progol_refine/2
progol_version/1
prove/6
prove/8
prove1/1
prove2/7
prove3/7
prove_at_least/5
prove_at_most/5
prove_cache/8
prove_cache/9
prove_cached/8
prove_cached/9
prove_examples/14
prove_intervals/6
prove_intervals/7
prove_lazy_cached/6
prove_neg/9
prove_pos/9
prove_rand/7
prune_open/3
quicksort/3
range_restrict/4
range_restriction/4
rdhyp/0
read_all/1
read_examples/1
read_examples/2
read_rules/1
record_clause/4
record_date/1
record_machine/1
record_nskolemized/4
record_sat_example/1
record_search_stats/3
record_settings/0
record_skolemized/5
record_targetpred/0
record_testclause/1
record_theory/1
reduce/0
reduce/1
reduce_prelims/3
refinement_ok/2
reinstate/1
remove1/2
remove2/2
remove_lits/1
rename/5
rename_ovars/6
renormalise/2
renormalise/3
reset/0
reset_best_label/0
reset_counts/0
reset_succ/0
restorehyp/0
retractall/2
reverse/2
revzap/3
rm_commutative/2
rm_interval/3
rm_intervals/3
rm_moderepeats/2
rm_seeds/0
rm_seeds/2
rm_seeds1/3
rm_special_consideration/2
rm_symmetric/2
rm_uselesslits/2
rmhyp/0
rsat/0
rselect_clause/3
sample/3
sat/1
sat/2
sat_prelims/0
search/2
select_example/4
set/2
set_lazy_negs/1
set_lazy_on_contradiction/2
set_lazy_recalls/0
set_up_builtins/0
setting/2
settings/0
show/1
show/2
show1/2
show_clause/4
show_stats/2
skolem_var/1
skolemize/2
skolemize/5
slprove/2
special_consideration/2
split_args/4
split_args1/5
split_clause/3
split_ok/3
split_vars/9
store/1
strip_true/2
subset1/2
suffix/2
sum_counts/2
symmetric/1
test/4
text/2
time/3
time_loop/2
ub_hashed_combinations/4
uniq_insert/4
update/3
update_argtypes/1
update_atoms/1
update_backpreds/1
update_best/7
update_besthyp/1
update_cache/3
update_coverset/2
update_coversets/4
update_dependents/2
update_distribution/2
update_equiv_lists/3
update_equivs/2
update_estimate_nclauses/1
update_estimate_variants/1
update_gsample/2
update_implied/2
update_iterms/2
update_list/3
update_lit/6
update_max_head_count/2
update_modetypes/2
update_open_list/4
update_oterms/4
update_probabilistic_refinement/7
update_theory/1
update_types/1
val/2
val1/2
vars_in_term/3
worse_coversets/4
worse_coversets1/4
write_cmatrix/1
write_entry/2
write_profile_data/1
write_rules/1

Commands and parameters Index

Jump to: a - b - c - d - e - f - g - h - i - l - m - n - o - p - r - s - t - u - v - w

a

  • addhyp/0
  • b

  • best
  • bf search
  • c

  • caching
  • check_implication/1
  • clauselength
  • commutative/1
  • compression
  • condition
  • construct_bottom
  • cost/3
  • coverage
  • covers/0
  • coversn/0
  • d

  • depth
  • determination/2
  • determinations/2
  • df search
  • e

  • evalfn
  • example_saturated/1
  • explore
  • explore_tolerance
  • f

  • false/0, false/0
  • g

  • gsamplesize
  • h

  • heuristic search
  • hypothesis/3
  • i

  • i
  • ibs search
  • ils search
  • induce/0
  • induce_cover/0
  • induce_max/0
  • l

  • laplace
  • lazy_evaluate/1
  • lazy_negs
  • lazy_on_contradiction
  • lazy_on_cost
  • m

  • m
  • m estimate (automatic m setting)
  • m estimate (user set m)
  • man/1
  • minacc
  • minpos
  • mode/2
  • modeb/2
  • modeh/2
  • modes/2
  • n

  • nodes
  • noise
  • noset/0
  • o

  • openlist
  • p

  • pbayes (pseudo-Bayes estimate)
  • positive_only/1
  • posonly (positive only evaluation)
  • pretty_print
  • print
  • proof_strategy
  • prune/1
  • r

  • rdhyp/0
  • read_all/0
  • record
  • recordfile
  • reduce/0
  • refine
  • refine/2
  • s

  • samplesize
  • sat/1
  • search
  • set/2
  • setting/2
  • show/1
  • skolemvars
  • splitvars
  • stage
  • symmetric/1
  • t

  • test/4
  • test_neg
  • test_pos
  • text/2
  • train_neg
  • train_pos
  • u

  • user (cost function)
  • v

  • verbose
  • verbosity
  • version
  • w

  • write_rules/1
  • Concept Index

    Jump to: b - c - d - e - g - h - i - l - m - n - p - r - s - t - v - w - y

    b

  • Background knowledge file
  • Basic algorithm
  • Beam search
  • Breadth-first search strategy
  • c

  • Caching clause coverage
  • Changes made across versions of P-Progol
  • Changing the evaluation function
  • Changing the proof strategy
  • Changing the search
  • Clause length restriction
  • Conditioning random sample
  • Constraint specification
  • Constructing a theory
  • Cost specification
  • CProgol
  • d

  • Depth-first search strategy
  • Determinations
  • e

  • Evaluating a theory
  • Evaluation functions
  • Exploratory mode
  • Exploratory mode with tolerance
  • g

  • Getting started with P-Progol
  • Greedy search
  • h

  • Heuristic search strategy
  • How Sicstus Progol Compiles Examples
  • How to Express Constraints in Sicstus Progol
  • i

  • Indlog
  • Iterative beam search strategy
  • Iterative language search strategy
  • l

  • Lazy bottom clause generation
  • Lazy coverage evaluation
  • Lazy evaluation
  • Lazy negative coverage evaluation
  • Loading P-Progol
  • m

  • M estimation
  • Maximum negative coverage
  • Maximum nodes searched
  • Minimum clause accuracy
  • Minimum positive coverage
  • Mode declarations
  • n

  • Negative examples file
  • Negative examples for testing
  • Negative examples for training
  • No Auto Set of lazy_on_cost in Sicstus Progol
  • No Depth Bound in Sicstus Progol
  • p

  • Positive examples file
  • Positive examples for testing
  • Positive examples for training
  • Positive Only Learning in Sicstus Progol
  • Positive-only learning
  • Predicates used in P-Progol
  • Pretty printing
  • Pruning
  • r

  • Random sample size
  • Reading input files
  • Reducing a single bottom clause
  • Reduction
  • Reference Manual
  • Refinement operator specification
  • Refinement operator types
  • Related versions and programs
  • Running Sicstus P-Progol
  • s

  • Samples greater than 1
  • Saturating a single example
  • Saturation
  • Saving a theory
  • Search commands and options
  • Search strategies
  • Setting a minimum score
  • Setting parameter values
  • Show things
  • Sicstus version of P-Progol
  • Skolem variable numbering in examples
  • SWI version of P-Progol
  • t

  • T-Reduce
  • Theorem-proving depth
  • Type specifications
  • v

  • Variable chain depth
  • Verbosity
  • Version
  • w

  • Writing trace to a file
  • y

  • Yap version of P-Progol
  • Predicates Index

    Jump to: a - b - c - d - e - f - g - h - i - l - m - n - o - p - q - r - s - t - u - v - w

    a

  • abandon_branch/2
  • add_backs/1
  • add_cache/3
  • add_eqs/4
  • add_eqs/5
  • add_equivalences/3
  • add_generator/2
  • add_hyp/1
  • add_hyp/4
  • add_ioc_links/4
  • add_lit/8
  • add_litinfo/6
  • add_new_lit/8
  • add_ovars/2
  • add_prune_cache/1
  • add_skolem_types/1
  • add_skolem_types/3
  • add_skolem_types1/2
  • add_skolem_types2/2
  • add_types/1
  • addhyp/0
  • app_lit/3
  • append/3
  • apply_equivs/6
  • assemble_label/4
  • b

  • best_hypothesis/3
  • binom/4
  • binom_lte/4
  • built_in_prune/1
  • c

  • calc_intersection/3
  • call_library_pred/6
  • check_auto_refine/0
  • check_cache/3
  • check_implication/1
  • check_parents/4
  • check_posonly/0
  • check_prune_defs/0
  • check_user_search/0
  • choose/3
  • clause_distribution/2
  • clause_ok/3
  • clause_to_list/2
  • clean_up/0
  • clean_up_reduce/0
  • clean_up_sat/0
  • clear_cache/0
  • clear_hyp/0
  • collect_args/2
  • collect_example_cache/1
  • commutative/1
  • complete_clause_label/4
  • compression_ok/2
  • concat/2
  • condition/1
  • condition_target/0
  • construct_call/4
  • construct_incall/4
  • construct_name/3
  • construct_prolog_name/2
  • continue_search/3
  • copy_args/3
  • copy_args/4
  • copy_consts/3
  • copy_var/3
  • cost_cover_required/0
  • covers/0
  • covers/1
  • coversn/0
  • coversn/1
  • d

  • dappend/3
  • declare_dynamic/1
  • delete/3
  • delete0/3
  • delete1/3
  • delete_all/3
  • delete_list/3
  • depth_bound_call/1
  • determination/2
  • do_precomputation/0
  • e

  • equal_set/2
  • estimate_error/6
  • estimate_error_rate/5
  • estimate_variants/2
  • eval_rule/2
  • evalfn/2
  • evalfn/3
  • evalfn_name/2
  • evaluate/6
  • example/3
  • example_saturated/1
  • examples/2
  • execute/1
  • execute_equality/1
  • expand/12
  • explore_eq/2
  • extend_clause/3
  • extract_count/3
  • extract_cover/2
  • extract_cover/3
  • extract_length/2
  • extract_neg/2
  • extract_pos/2
  • f

  • find_beta_prob/2
  • find_count/2
  • find_hashed_variants/3
  • find_lazy_left/4
  • find_max_values/3
  • find_max_width/3
  • find_posgain/2
  • fix_base/2
  • flatten/5
  • flatten_args/5
  • flatten_atom/10
  • flatten_eq/7
  • flatten_lit/8
  • flatten_lits/11
  • flatten_terms/2
  • g

  • gen_auto_refine/0
  • gen_layer/2
  • gen_lit/1
  • gen_lits/2
  • gen_refine_id/1
  • gen_sample/2
  • gen_var/1
  • get_args/4
  • get_argterms/4
  • get_atoms/5
  • get_atoms1/5
  • get_besthyp/0
  • get_c_links/4
  • get_cache_entry/3
  • get_clause/4
  • get_determs/2
  • get_eqs/6
  • get_equivs/2
  • get_flatatom/4
  • get_gain/16
  • get_gain1/15
  • get_gains/15
  • get_hyp/1
  • get_hyp_label/2
  • get_i_links/5
  • get_implied/0
  • get_implied/3
  • get_ivars/3
  • get_ivars1/2
  • get_marked/3
  • get_max_negs/3
  • get_modes/2
  • get_next_atom/1
  • get_nextbest/1
  • get_node/4
  • get_nsuccesses/2
  • get_o_links/5
  • get_ovars/3
  • get_ovars1/2
  • get_pclause/6
  • get_pclause1/6
  • get_performance/0
  • get_predecessors/3
  • get_predicates/3
  • get_progol_clause/2
  • get_progol_lit/2
  • get_progol_lit/3
  • get_progol_lits/2
  • get_psyms/2
  • get_random/2
  • get_refine_gain/12
  • get_refine_id/2
  • get_repeats/3
  • get_search_keys/3
  • get_search_settings/1
  • get_sibgain/18
  • get_sibgains/15
  • get_sibpncover/7
  • get_start_label/2
  • get_successes/2
  • get_type_name/2
  • get_unmarked/3
  • get_user_refinement/4
  • get_var_equivs/6
  • get_vars/3
  • get_vars_in_term/2
  • goals_to_clause/2
  • goals_to_list/2
  • gsample/2
  • h

  • has_hashed/4
  • has_hashed_loc/2
  • hash_term/2
  • hashed_combinations/2
  • hashed_variant/3
  • hashed_variants/3
  • hypothesis/3
  • i

  • in_path/1
  • inc_beta_count/2
  • inc_beta_counts/2
  • inc_count/1
  • index_clause/3
  • index_prove/6
  • index_prove/8
  • index_prove1/6
  • index_prove1/9
  • induce/0
  • induce_cover/0
  • induce_max/0
  • induce_max/1
  • induce_max1/1
  • insert_eqs/3
  • integrate_args/3
  • integrate_args/4
  • integrate_head_lit/1
  • integrate_term/2
  • integrate_term/3
  • integrate_terms/3
  • intersect1/4
  • intersects/2
  • interval_count/2
  • interval_intersection/3
  • interval_subsumes/2
  • interval_subtract/3
  • interval_to_list/2
  • intervals_intersection/3
  • intervals_intersects/2
  • intervals_intersects/3
  • intervals_intersects1/2
  • intervals_intersects1/3
  • intervals_to_list/2
  • is_symmetric/3
  • l

  • label_create/2
  • label_create/3
  • label_ncover/2
  • label_pcover/2
  • label_print/1
  • label_union/3
  • lang_ok/2
  • lang_ok1/2
  • lazy_evaluate/1
  • lazy_evaluate/6
  • lazy_evaluate1/7
  • lazy_evaluate_refinement/5
  • lazy_evaluate_refinement/6
  • lazy_index_prove/4
  • lazy_index_prove1/4
  • lazy_prove/4
  • lazy_prove_neg/9
  • lazy_prove_negs/3
  • legal_term/4
  • length_ok/6
  • list_profile/0
  • list_to_clause/2
  • list_to_goals/2
  • list_to_interval/4
  • list_to_intervals/2
  • list_to_intervals1/2
  • lit_redun/2
  • m

  • make_sname/2
  • man/1
  • mark_lit/6
  • mark_lits/3
  • mark_lits/7
  • match_body_modes/1
  • match_bot/3
  • match_bot_lit/2
  • match_bot_lits/3
  • match_lazy_bottom/2
  • match_lazy_bottom1/1
  • match_mode/2
  • maxcovers/1
  • maxcoversn/1
  • maxlength_neg_ok/4
  • member/2
  • member1/2
  • member2/2
  • merge_vlist/2
  • mincovers/1
  • mincoversn/1
  • modeb/2
  • modeh/2
  • n

  • next_node/2
  • nlits/2
  • noset/1
  • o

  • occurs1/4
  • occurs_in/2
  • p

  • p1_message/1
  • p_message/1
  • partition/4
  • pfac/4
  • pos_ok/6
  • positive_only/1
  • pp_dclause/1
  • pp_dclause/2
  • pp_dlist/1
  • pp_dlist/2
  • prefix_lits/3
  • print_eval/2
  • print_lit/6
  • print_litlist/4
  • print_lits/4
  • print_node_count/2
  • print_text/1
  • probabilistic_extend/3
  • probabilistic_extensions/2
  • process_determs/0
  • process_mode/1
  • process_modes/0
  • progol_get_hlit/2
  • progol_get_lit/2
  • progol_has_ovar/3
  • progol_has_ovar1/4
  • progol_help/0
  • progol_help/1
  • progol_manual/1
  • progol_portray/1
  • progol_portray/2
  • progol_refine/2
  • progol_version/1
  • prove/6
  • prove/8
  • prove1/1
  • prove2/7
  • prove3/7
  • prove_at_least/5
  • prove_at_most/5
  • prove_cache/8
  • prove_cache/9
  • prove_cached/8
  • prove_cached/9
  • prove_examples/14
  • prove_intervals/6
  • prove_intervals/7
  • prove_lazy_cached/6
  • prove_neg/9
  • prove_pos/9
  • prove_rand/7
  • prune_open/3
  • q

  • quicksort/3
  • r

  • range_restrict/4
  • range_restriction/4
  • rdhyp/0
  • read_all/1
  • read_examples/1
  • read_examples/2
  • read_rules/1
  • record_clause/4
  • record_date/1
  • record_machine/1
  • record_nskolemized/4
  • record_sat_example/1
  • record_search_stats/3
  • record_settings/0
  • record_skolemized/5
  • record_targetpred/0
  • record_testclause/1
  • record_theory/1
  • reduce/0
  • reduce/1
  • reduce_prelims/3
  • refinement_ok/2
  • reinstate/1
  • remove1/2
  • remove2/2
  • remove_lits/1
  • rename/5
  • rename_ovars/6
  • renormalise/2
  • renormalise/3
  • reset/0
  • reset_best_label/0
  • reset_counts/0
  • reset_succ/0
  • restorehyp/0
  • retractall/2
  • reverse/2
  • revzap/3
  • rm_commutative/2
  • rm_interval/3
  • rm_intervals/3
  • rm_moderepeats/2
  • rm_seeds/0
  • rm_seeds/2
  • rm_seeds1/3
  • rm_special_consideration/2
  • rm_symmetric/2
  • rm_uselesslits/2
  • rmhyp/0
  • rsat/0
  • rselect_clause/3
  • s

  • sample/3
  • sat/1
  • sat/2
  • sat_prelims/0
  • search/2
  • select_example/4
  • set/2
  • set_lazy_negs/1
  • set_lazy_on_contradiction/2
  • set_lazy_recalls/0
  • set_up_builtins/0
  • setting/2
  • settings/0
  • show/1
  • show/2
  • show1/2
  • show_clause/4
  • show_stats/2
  • skolem_var/1
  • skolemize/2
  • skolemize/5
  • slprove/2
  • special_consideration/2
  • split_args/4
  • split_args1/5
  • split_clause/3
  • split_ok/3
  • split_vars/9
  • store/1
  • strip_true/2
  • subset1/2
  • suffix/2
  • sum_counts/2
  • symmetric/1
  • t

  • test/4
  • text/2
  • time/3
  • time_loop/2
  • u

  • ub_hashed_combinations/4
  • uniq_insert/4
  • update/3
  • update_argtypes/1
  • update_atoms/1
  • update_backpreds/1
  • update_best/7
  • update_besthyp/1
  • update_cache/3
  • update_coverset/2
  • update_coversets/4
  • update_dependents/2
  • update_distribution/2
  • update_equiv_lists/3
  • update_equivs/2
  • update_estimate_nclauses/1
  • update_estimate_variants/1
  • update_gsample/2
  • update_implied/2
  • update_iterms/2
  • update_list/3
  • update_lit/6
  • update_max_head_count/2
  • update_modetypes/2
  • update_open_list/4
  • update_oterms/4
  • update_probabilistic_refinement/7
  • update_theory/1
  • update_types/1
  • v

  • val/2
  • val1/2
  • vars_in_term/3
  • w

  • worse_coversets/4
  • worse_coversets1/4
  • write_cmatrix/1
  • write_entry/2
  • write_profile_data/1
  • write_rules/1

  • This document was generated on 29 September 1999 using the texi2html translator version 1.52.