Information Technology Reference
In-Depth Information
If we use P
∧
P' to replace P* (here P' is a predicate constant with the same
number of variables of that of P), then CIRC(T, P) can be writed as:
∀
x(P(x)
∧
P'(x)
P(x))
∀
x)(P(x)
P(x)
∧
P'(x))
ϕ
P
=T(P
∧
P')
(2.10)
And therefore we get the following formula:
T(P
∧
P')
(
∀
x)(P(x)
P'(x))
(2.11)
If we replace (
∀
x)(P*x)
P(x)) by P*
X
P, then:
P
*
X
P represent (P
*
X
P)
∧
¬(P
X
P
*
), and
P
*
= P represent (P
*
X
P)
∧
(P
X
P
*
)
And therefore we get
∀
P
*
(T(P
*
)
∧
(P
*
X
P)
(P
X
P
*
))
ϕ
P
=
(2.12)
∀
P
*
(T(P
*
)
¬ (P
*
X
P))
I.e.,
ϕ
P
=
= ¬ (
∃
P
*
)(T(P
*
)
∧
(P
*
X
P))
(2.13)
Theorem 2.5
Let T be a formula of a first-order language, and let P be a
predicate contained in T. Then, for any P' such that T(P)
ũ
X
P), it
T(P')
∧
(P'
must be
CIRC(TP) = T(P)
∧
(P = P')
(2.14)
According to this theorem, if T(P')
∧
(P'
X
P) can be deduced from T(P), then
P = P' is the circumscription formula of P in T.
2.7 Nonmonotonic Logic NML
The nonmonotonic logic NML proposed by McDermott and Doyle is a general
default logic for the study of general foundation of nonmonotonic logics
(McDermott,1980). McDermott and Doyle modify a standard first-ordet logic by
introducing a modal operator
¾
, which is called compatibility operator. For
example, the following is a formula of NML:
∀
x
(Bird(
x
)∧
¾
Fly(
x
)
ã
Fly(
x
))
