Download pdf - arXiv

2.6. Previous approaches for coding logical theories
2.6.2
29
The Proof Complexity Approach
The other approach for L(E|T ) was proposed by Muggleton, Srinivasan and
Bain in 1992 [36] called the “proof complexity” measure (PC), defined as the
bits required to code the proof of each example given the theory. The proof
complexity of an example e is calculated as the sum of the logarithm of the
choice-points involved in the SLD-refutation of e. In each step of a refutation,
if G is the actual goal, the choice-points are the number of program clauses
whose heads unify with the atom of G selected by the selection function.
Therefore,
X
LPC (A|T )
(2.22)
LPC (E|T ) =
A∈E
where LPC (A|T ) is the code length of an atom A wrt. a theory T .
In this case, only the given evidence is coded, never the absent examples
(those elements in Q(T ) which are not in E). This is counter-intuitive, since
LPC (E|T ) > 0 when Q(T ) = E. Even with a perfect-covering program, we
have that LPC (E|T ) is not zero.
The following chapter is then devoted to a coding scheme which considers
programs with function symbols (for both L(T ) and L(E|T )) and tries to
solve the problems of both the MC and PC approaches.
Also, one of the important things of a coding scheme, especially if it is
used for theory selection, is that it must be as efficient as possible. The MC
and PC approaches, as we will see, contain several sources of redundancy in
their codes.