cProgol page at Imperial PROGOL employs a covering approach like, e.g., FOIL. That
is, it selects an example to be generalised and finds a consistent clause
covering the example. All clauses made redundant by the found clause including
all examples covered by the clause are removed from the theory. The example
selection and generalisation cycle is repeated until all examples are covered.
When constructing hypothesis clauses consistent with the examples, PROGOL
conducts a general-to-specific search in the theta-subsumption lattice
of a single clause hypothesis. In contrast to other general-to-specific
searching systems, PROGOL computes the most specific clause covering the
seed example and belonging to the hypothesis language. This most specific
clause bounds the theta-subsumption lattice from below. On top, the lattice
is bounded by the empty clause. The search strategy is an A*-like
algorithm guided by an approximate compression measure. Each invocation
of the search returns a clause which is guaranteed to maximally compress
the data, however, the set of all found hypotheses is not necessarily the
most compressive set of clauses for the given example set. PROGOL can learn
ranges and functions with numeric data (integer and floating point) by
making use of the built-in predicates ``is'', <, =<, etc.
The hypothesis language of PROGOL is restricted by the
means of mode declarations provided by the user. The mode declarations
specify the atoms to be used as head literals or body literals in hypothesis
clauses. For each atom, the mode declaration indicates the argument types,
and whether an argument is to be instantiated with an input variable, an
output variable, or a constant. Furthermore, the mode declaration bounds
the number of alternative solutions for instantiating the atom. The types
are defined in the background knowledge by unary predicates, or by Prolog
built-in functions.