Information Technology Reference
In-Depth Information
In expressive power FO(=(
...
)) is equivalent to existential second-order logic
(ESO) [2]. For some variants of FO(=(
...
)), the correspondence with ESO does
not hold or it can depend on which version of team semantics is being used. For
instance, FO(
) corresponds in expressive power to ESO if we use the so-called
“strict team semantics” [4]. Under the lax team semantics, FO(
ↆ
) corresponds
to greatest fixed-point logic (GFP) [5] which captures PTIME over finite ordered
models. In FO(=(
...
)) no separation between the strict and the lax version of
team semantics exists since dependence atoms satisfy the so-called downward
closure property. In the following we briefly list some complexity theoretical
aspects of FO(=(
...
)) and its variants.
ↆ
-
FO(=(
...
)) extended with the so-called intuitionistic implication
→
(intro-
duced in [6]) increases the expressive power of FO(=(
...
)) to full second-order
logic [7].
-
The model checking problem of FO(=(
...
)), and many of its variants, was
recently shown to be NEXPTIME-complete. Moreover, for any variant of
FO(=(
...
)) whose atoms are PTIME-computable, the corresponding model
checking problem is contained in NEXPTIME [8].
-
The non-classical interpretation of disjunction in FO(=(
...
)) has the effect
that the model checking problems of
ˆ
1
:= =(
x, y
)
∨
=(
u,v
)and
ˆ
2
:=
=(
x, y
)
∨
=(
u,v
)
∨
=(
u,v
) are already NL-complete and NP-complete,
respectively [9].
This article pursues the line of study taken in [10,4] where syntactical fragments
of dependence and independence logic (FO(
↥
c
)) were investigated, respectively.
FO(
↥
c
) extends first-order logic by conditional independence atoms
y
↥
x
z
with the informal meaning that the values of
y
and
z
are independent of each
other, given any value of
↥
c
) does not have downward
closure and is sensitive to the choice between the lax and the strict version of
team semantics. For a set of atoms
x
.AsFO(
ↆ
), also FO(
C
,weuseFO(
C
) (omitting the set parentheses
of
C
) to denote the logic obtained by adding the atoms of
C
to first-order logic.
)inwhichatmost
k
variables are
universally quantified. In [10] it was shown that
C
)(
k
∀
C
FO(
) denotes the sentences of FO(
FO(=(
...
))(
k
∀
)
≤
ESO
f
(
k
∀
)
≤
FO(=(
...
))(2
k
∀
)
where ESO
f
(
k
) denotes the Skolem normal form ESO sentences in which at
most
k
universally quantified first-order variables appear. In [4] it was shown
that (under the lax team semantics)
∀
-
FO(
↥
∀
↥
)(2
)=FO(
)and
-
FO(
↥
,
ↆ
)(1
∀
)=FO(
↥
,
ↆ
)
where FO(
↥
) is the sublogic of FO(
↥
c
) allowing only so-called pure independence
atoms
x
↥
y
. Moreover, it is known that FO(
↥
) is equivalent in expressive power
to FO(
↥
,
ↆ
)andFO(
↥
c
) [1,11].
