Information Technology Reference

In-Depth Information

F

E

F

E

A

=
A
E

C

C

(b)

Γ

B ⊗ C
D

C
E ⊗ F

(a)

(c)

Fig. 3.
Γ

(a), constraint graph for CSA
Γ
;
A ⊗ B ⊗ C F

(b), and constraint graph

for CSA
Γ
;
A ⊗ C F ⊗ E
2
(c).

3.2

Removing Redundant CSCs

After the possibly required literals have been determined, we can throw away all

CSCs, which include at least one literal which is not included in the constraint

graph. In that way the search space would be pruned and search made more

ecient. Provability of a particular CSA would not be affected by removing

these CSCs.

Theorem 2.
Given a CSA and a set of edges
D
e
of the constraint graph

,

which was constructed for the CSA, we can discard all CSCs
c ∈ Γ
,which

satisfy condition

D

∃l.
((
l ∈

∨ l ∈

∧ l ∈ D
e
∧

≡∅

succ
(
c
)

ant
(
c
))

succ
(
c
)

)
without

affecting the provability of the CSA.

Proof.
If there is a CSC
c ∈ Γ
of a CSA such that

∃l.
((
l ∈

∨ l ∈

ant
(
c
)

succ
(
c
))

∧ l ∈ D
e
), then it means that
c
was not considered during construction

of constraint graph

. Therefore
c
is not considered relevant for finding a proof

for the particular CSA and can be discarded.

D

CSC reduction is illustrated in Fig. 3(c), where a constraint graph is gen-

erated for CSA
Γ
;
A ⊗ C F ⊗ E
2
. Since literals
B
and
D
are not present in

the constraint graph, they are considered irrelevant for PD. Therefore all CSCs

c
such that
B ∈

succ
(
c
)canbe

removed without affecting the provability result of the original problem. Hence

ant
(
c
)or
D ∈

ant
(
c
)or
B ∈

succ
(
c
)or
D ∈

B

⊗

C

D
can be removed from
Γ
.

3.3 The Computational Complexity

of Constructing Abstraction Hierarchies

According to [7] the complexity of building the constraint graph is
O
(
n

l
),

where
n
is the number of different literals in a CSC,
o
is the maximum number

of CSCs relevant for achieving any given literal, and
l
is the total number of

different literals in succedents of relevant CSCs. Building a hierarchy is also

O
(
n

∗

o

∗

l
) since the number of edges in the graph is bounded by
n ∗ o ∗ l
and

the complexity of the graph algorithms used is linear.

∗

o

∗

4

PD with Abstraction Hierarchies

To prove hierarchically, sequents are first mapped to the highest level of ab-

straction. This is done by substituting literals, not essential at that abstraction

Search WWH ::

Custom Search