Information Technology Reference
In-Depth Information
description acquired from the explanation is specialization of goal concept and
generalization of example, which makes the result not too generalizable and can
be used commonly.
9.6 Logic Program of Explanation-Based Generalization
As mentioned in previous sections, an explanation structure about the training
examples should be established first in EBG. This is actually a theorem proving
problem thus EBG can be regarded as the extension of resolution theory prove of
Horn clauses and the generalization can be considered as the attachment of
standard theorem proving.
9.6.1
Operational principle
The logic program design language, for example Prolog and so on are based on
resolution principle. The main point of resolution principle is to check out
whether the set of clauses contains null clause. Virtually, resolution principle is a
kind of deductive rule by which the result clauses are created from the clauses
set.
Resolution principle: Given initial clauses C
1
and C
2
and there is no common
variables, L
1
and L
2
are two literals of C
1
and C
2
respectively. If there is a most
general unifier of L
1
and ¬L
2
, then clause (C
1
- L
1
)
∨
(C
2
- L
2
) is denoted as the
resolvent of C
1
and C
2.
For a given goal, the detailed process of searching for clause match of Turbo
Prolog is a unified process, which completes the parameter transmission in other
programming language. The following is the unified algorithm:
Algorithm 9.2
: The unification algorithm of Turbo Prolog
(1) Free variable can be unified with other tem arbitrarily. The free variable
becomes the bounded unified term after unification.
(2) Constant can be unified with itself or free variables.
(3) If functor of two compound terms are the same and with same number of
parameter, then the unification can be done under the condition that every
sub-term can be unified correspondingly. The bounded variable should be
substituted with unified bounded value.
The first thing EBG need to do is to create explanation structure of training
examples, that is taking the training example as target, acquiring a proof of the
training examples by searching and matching the domain theory (the domain
