Information Technology Reference
In-Depth Information
Let FC be a first order predicate calculus system with the compatibility
operator ¾ embraced in, and let LFC be the set of all the formulas of FC. Then,
for any set Γ ⊆ LFC, Th(Γ ) is defined as:
Th(Γ ) = {A | Γ |- FC A}
Th(Γ) can also be defined according to another approach. For any set S⊆LFC,
a nonmonotonic operator NMΓ is firstly defined as:
NM Γ (S) = Th(Γ ∪ ASM Γ (S))
Where ASMΓ (S) is the assumption set of S and is defined as:
ASM Γ (S)={ ¾ Q| Q ∈ L FC ∧ ¬Q∉S}
Then, Th(Γ) can be defined as:
Th(Γ ) = ∩ ({L FC } ∪ {S | NM Γ (S) =S})
According to this definition, we can see that Th(Γ) is the intersection of all
fixed points of NMΓ, or the entire language if there are no fixed points.
Now, the nonmonotonic inference |~ can be defined as: Γ|~ P if and only if
P∈Th(Γ).
It should be noted that Γ|~P requires that P is contained in each fixed point of
NMΓ in the case that there are fixed points. However, in default theory, what is
needed for P to be provable in ∆ is juat that P is contained in one of ∆'s extension,
i.e., P is contained in one of the fixed points.
Example 2.10 Suppose Γ is an axiom theory which contains ¾ P ã ¬Q and
¾ Q ã ¬P, i.e.:
= FC∪ { ¾ P ã ¬Q, ¾ Q ã ¬P }
Then there are two fixed points for this theory: (P, ¬Q) and (¬P, Q).
Γ
However, for another theory Γ = FC∪{ ¾ P ã ¬P}, we can demonstrate that it
has no fixed points. The demonstration is as follows. Suppose NMΓ (S)=S'. If
¬P∉S then we will have ¾ P∈ASMΓ (S) and consequently ¬P∈S'; On the
contrary, if ¬P∈S then we will have ¾ P∉ASMΓ (S), and consequently ¬P ∉S'.
Therefore, S will never be equal with S', i.e., there is no fixed point for NMΓ.
The aboving phenomenon can be further explained according to the following
results:
{ ¾ P ã ¬Q, ¾ Q ã ¬P } |~ ¬P ∨¬Q
{ ¾ P ã ¬P} |~ contradiction
McDermott and Doyle pointed out the following two problems on the
reasoning process of NML:
Search WWH ::




Custom Search