Information Technology Reference
In-Depth Information
(2) if Γ 1 ⊆Γ 2 , then Th(Γ 1 ) ⊆ Th(Γ 2 )
(3) Th(Th(Γ)) = Th(Γ) (idempotence)
Where (3) is also called as fixed point. A marked feature of monotonic inference
rules is that the language determined by them is a bounded least fixed point, i.e.,
Th(Γ 1 ) = ∩ {s | Γ 1 →S and Th(S) = Γ 2 }.
In order to deal with the property of nonmonotonic, the following inference
rule is introduced:
(4) if Γ¬
¬ P, then Γ |∼ MP
Here M is a modal operator. The rule states that if ¬P can not be deduced from Γ,
then P is in default treated as true.
It is obvious that a fixed point Th(Γ) = Γ can not be guaranteed any more as
while as the inference rule (4) is incorporated into monotonic inference
systems. In order to solve this problem, we can first introduce an operator
NM as follows: for any first-order theory Γ and any formula set S ⊆ L, set
(5) NMΓ(S) = Th(Γ ∪ ASΓ(S))
Where ASΓ(S) is a default set of S and is defined as follows:
(6) ASΓ(S) = {MP |P ∈ L P ∈ S}Th(Γ)
Then, Th(Γ ) can be defined as the set of theorems that can be deduced from
Γ nonmonotonically, i.e.,
(7) Th(Γ) = the least fixed point of NMΓ
Rule (7) is designed to blend the inference rule (4) into the first-order theory Γ so
that reasoning can be carried out with a closed style. However, since the
definition of Th(Γ) is too strong, not only the calculation but also the existence of
Th(Γ) can not be guaranteed. Therefore, definition of Th(Γ) is revised as follows:
(8) Th(Γ) = ∩({L}∪{S|NMΓ(S)=S})
Now, let L be the language determined by these rules, then L must be a fixed
point according to NMΓ (L) = L.
Search WWH ::




Custom Search