Information Technology Reference
In-Depth Information
The imperfect of domain theory may involve the following conditions:
(1) IncompleteLack of rules and knowledge in the domain theory thus no
explanation of training example can be given.
(2) Incorrect Some rules in the domain theory is unreasonable thus incorrect
explanation might be created.
(3) IntractableDomain theory is too complex; the existing resource can not
afford to create an explanation tree for training examples.
In order to solve the problem of imperfect domain theory, we make some
attempts in inverting resolution and deep knowledge based approach.
9.9.2
Inverting Resolution
Resolution theorem in first order logic is the foundation of machine theorem
proving and the main way to construct explanation in EBL(Muggleton etal.,
1988).
Resolution theoremLet C
1
,C
2
be two clauses without any common variables.
L
1
, L
2
are two literals of C
1
and C
2
respectively, if there is a most general unifier
Ŏ
, then clause
C= (C
1
- {L
1
})
Ŏ
∪
(C
2
- {L
2
})
Ŏ
(9.2)
is the resolution clause of C
1
and C
2
.
Inverting resolution deals with that given C and C
1
how to obtain C
2
. In
propositional logic,
Ŏ
Ŋ
, so the inverting clause (9.2) can be converted into:
C =(C
1
∪
C
2
) - {L
1
,L
2
}
(9.3)
From formula (9.3), the following formulas can be concluded
(1) if C
1
ŝ
C
2
=
, then C
2
= (C-C
1
)
∪
{L
2
}
(2) if C
1
ŝ
C
2
¬
, C
2
needs to contain the arbitrary sub-set of C
1
-{L
1
},
therefore, generally speaking:
C
2i
= (C - C
1
)
∪
{L
2
}
∪
S
1i
(9.4)
) represents the power set of set x.
It is obvious if there are n literals in C
1
, the number of solution for C
2
is 2n-1.
In the first order logic, let
Ŏ
=
ȶ
1
ȶ
2
,
ȶ
1
and
ȶ
2
satisfy
(1) The variable domain of
ȶ
1
and
ȶ
2
is domain of C
1
and domain of C
2
respectively.
Here, S
1i
∈
P (C
1
-{L
1
}, P(
x
(2)
L
ȶ
1
=
L
ȶ
2
1
2
Therefore:
C
2
= (C-(C
1
-{L
1
})
ȶ
1
)
ȶ
2
-1
L
}
ȶ
1
ȶ
2
-1
∪
{
1
L
}
ȶ
1
))
ȶ
2
-1
= ((C - (C
1
-{
ȶ
1
})
ȶ
1
)
∪
{
(9.5)
1
