Information Technology Reference
In-Depth Information
In this sense, an "atomic" axiom in the above sense, i.e. an axiom
A
for which the set
ζ
(
A
)
is
singleton, is said to be
irreducible
. For example, the formula
A
B
is irreducible, as it involves
only a single connective between two literals. On the contrary, the formula
A
∧
→∃
(
)
∧
x
:
p
x
(
)
q
involves a quantifier, an implication and two unary predicates, and is therefore reducible.
This formula can be decomposed into
x
ζ
(
A
)=
{
A
→
X
,
X
→∃
x
:
R
(
x
)
,
R
(
x
)
≡
P
(
x
)
∧
Q
(
x
)
,
P
≡
p
(
x
)
,
Q
≡
q
(
x
)
}
,
which is a set of irreducible axioms. For sets
C
of axioms, we define
ζ
(
C
)=
ζ
(
A
)
. Such
A∈
C
a decomposition is called
irreducible
, if each of its elements is irreducible.
For example, the statement
p(A) :- (q(A,B), r(B)) ; s(A)
is irreducibly decomposed into the set
ζ
being
{
X
0
→
X
1
,
X
0
≡
p
(
X
2
)
,
X
2
≡
A
,
X
1
≡
X
3
∨
X
4
,
X
3
≡
X
5
∧
X
6
,
X
5
≡
q
(
X
7
,
X
8
)
,
(2)
X
7
≡
A
,
X
8
≡
B
,
X
6
≡
r
(
X
9
)
,
X
9
≡
B
,
X
4
≡
s
(
X
10
)
,
X
10
≡
A
}
.
In the light of these considerations, the next result is immediately clear:
A
Lemma 3.1.
Let G be a non-ambiguous grammar satisfying the assumption above, and let
denote
an axiom in L
(
G
)
. Then there is a unique set of axioms of the form p
(
X
,
Y
1
,...,
Y
n
)
, where p is a
logical connective or a quantifier, and X
,
Y
1
,...,
Y
n
are literals.
We denote the decomposition implied by the lemma 3.1 by
ζ
(
A
)
ζ
(
A
)
. It is quite obvious that
A
A
is logically equivalent to
, as we can recover
by back-substituting the literals, which is
equivalent to stating that
and vice versa.
To ease notation, for logical implications or equivalences like
ζ
(
A
)
|
=
A
A
:
X
→
p
(
Y
1
,...,
Y
n
)
or
A
:
≡
(
)
(
A
)
(
A
)
X
p
Y
1
,...,
Y
n
, we write
lhs
to denote the set
{
X
}
, and
rhs
to collect all literals
A
(
A
)=
{
}
appearing on the right-hand side of
, i.e.
rhs
Y
1
,...,
Y
n
. Returning to the example
above, we would have
lhs
(
X
0
→
X
1
)=
{
X
0
}
and
rhs
(
X
0
→
X
1
)=
{
X
1
}
. For a set
C
of
)=
A∈
C
lhs
axioms, we set
lhs
is defined analogously.
As a mere technical tool, we introduce a graphic representation of the structure of an axiom.
It is closely related to the concept of parse-trees:
Definition 3.2
(structure graph)
.
Let
(
C
(
A
)
. The symbol
rhs
(
C
)
ζ
(
A
)
be an irreducible decomposition of an axiom. The vertices
of the
structure graph
G
s
A
G
s
are given by V
(
A
)=
lhs
(
ζ
(
A
))
, i.e. the vertices are the names of all
ζ
(
A
)
A
i
and
A
j
, if and only if
axioms that appear in
. The graph has an edge between two axioms
(
A
)
∩
(
A
)
=
∅
rhs
.
Graphically, the decomposition (2) would look like shown in figure 2. The vertices of the
structure graph are given by
lhs
lhs
i
j
, reading off the left-hand sides from the
decomposition (2). An arc is present between two vertices, if they appear on different sides of
the corresponding axiom, i.e.
X
0
and
X
1
are connected because the decomposition contains
the rule "
X
0
→
(
ζ
)=
{
X
0
,...,
X
10
}
X
1
".
This provides us with an adequate tool for simplifying axioms before putting it to the
diagnosis. Indeed, the structure graph's connectivity can be related to logical inconsistency:
Lemma 3.2
((Rass, 2005, Proposition 5.3.3))
.
Let C be a minimal conflict of an irreducible axiom
decomposition
ζ
(
C
)
. Then the corresponding structure graph is connected.
Search WWH ::
Custom Search