Information Technology Reference
In-Depth Information
A
clause
is a disjunction of literals. Let
C
and
D
be two clauses.
C
subsumes
D
if
there is a substitution
θ
such that
Cθ
D
.
C
properly subsumes
D
if
C
subsumes
D
but
D
does not subsume
C
.A
clausal theory
is a set of clauses, which is often identified
with the
conjunctive normal form
(CNF) formula composed by taking the conjunction
of all clauses in it. Let
Σ
be a clausal theory.
μΣ
denotes the set of clauses in
Σ
not
properly subsumed by any clause in
Σ
.A
consequence
of
Σ
is a clause entailed by
Σ
.
We denote by
Th
(
Σ
)
the set of all consequences of
Σ
.
The
consequence finding
problem was first addressed by Lee [18] in the context of
the resolution principle, which has the property that the consequences of
Σ
that are
derived by the resolution principle includes
μTh
(
Σ
)
. To find “interesting” theorems
for a given problem, the notion of consequence finding has been extended to the prob-
lem to find
characteristic clauses
[12]. Each characteristic clause is constructed over
a sub-vocabulary of the representation language called a “production field”. Formally,
a
production field
⊆
,where
L
is a set of literals closed under in-
stantiation, and
Cond
is a certain condition to be satisfied, e.g., the maximum length of
clauses, the maximum depth of terms, etc. When
Cond
is not specified,
P
is a pair,
L
,Cond
P
=
L
,
∅
is
simply denoted as
L
. A production field
P
is
stable
if, for any two clauses
C
and
D
such that
C
subsumes
D
,
D
belongs to
P
only if
C
belongs to
P
.
if every literal in
C
belongs to
L
and
C
satisfies
Cond
.Foraset
Σ
of clauses, the set of logical consequence of
Σ
belonging
to
Aclause
C
belongs to
P
=
L
,Cond
P
is denoted as
Th
P
(
Σ
)
. Then, the
characteristic clauses
of
Σ
with respect to
P
are defined as:
Carc
(
Σ,
P
)=
μTh
P
(
Σ
)
.
We here exclude any tautology
¬
L
∨
L
(
≡
True
)
in
Carc
(
Σ,
P
)
even when both
L
and
¬
L
belong to
P
.When
P
is a stable
production field, it holds that the empty clause
)
if and only if
Σ
is unsatisfiable. This means that theorem proving is a special case of
consequence finding. The use of characteristic clauses enables us to characterize various
reasoning problems of interest to AI, such as nonmonotonic reasoning, diagnosis, and
knowledge compilation as well as abduction and induction. In the propositional case
[20], each characteristic clause of
Σ
is a
prime implicate
of
Σ
.
When a new clause
C
is added to a clausal theory
Σ
, further consequences are de-
rived due to this new information. Such a new and “interesting” clause is called a “new”
characteristic clause. Formally, the
new characteristic clauses
of
C
with respect to
Σ
and
is the unique clause in
Carc
(
Σ,
P
Th
(
Σ
)]
.
When a new formula is not a single clause but a clausal theory or a CNF formula
F
=
C
1
∧···∧
P
are:
Newcarc
(
Σ,C,
P
)=
μ
[
Th
P
(
Σ
∧
C
)
−
C
m
, where each
C
i
is a clause,
Newcarc
(
Σ,F,
P
)
can be computed
as:
m
Newcarc
(
Σ,F,
P
)=
μ
[
Newcarc
(
Σ
i
,C
i
,
P
)]
,
(1)
i
=1
where
Σ
1
=
Σ
,and
Σ
i
+1
=
Σ
i
∧
1
. This incremental compu-
tation can be applied to get the characteristic clauses of
Σ
with respect to
C
i
,for
i
=1
,...,m
−
P
as follows.
Carc
(
Σ,
P
)=
Newcarc
(
True,Σ,
P
)
.
(2)
Several procedures have been developed to compute (new) characteristic clauses.
SOL
resolution
[12] is an extension of the Model Elimination (ME) calculus to which
Skip
