Class Description

FO(TC): First-order with transitive closure

FO(TC) is the set of boolean queries definable with first-order formulae with a transitive closure (TC) operator.

TC is defined this way: let be a positive integer and be vectors of variables, then TC( is true if there exist variables such that and for all . Here, is a formula over written in FO(TC) and means that the variables and are replaced by and .

Every formula of TC can be written in a normal form FO( where is a FO formula and we suppose that there is an order on the model where variables are quantified, so we can choose the minimum and maximum element.

It was shown in [Imm98] page 150 that this class is equal to NL.

Linked From

FO(DTC): First-order with deterministic transitive closure

FO(DTC) is defined as FO(tc) where the transitive closure operator is deterministic, which means that when we apply DTC(), we know that for all , there exist at most one such that phi(u,v).

We can suppose that DTC() is syntactic sugar for TC() where .

It was shown in [Imm98] on page 144 that this class is equal to L.

More about...


NL: Nondeterministic Logarithmic-Space

NL is to L as NP is to P. Not known whether a particular relation (equality or inequality) between P and NP implies the same relation between L and NL.

In a breakthrough result, was shown to equal coNL [Imm88] [Sze87]. (Though contrast to mNL.)

Is contained in LOGCFL [Sud78], as well as NC2.

Is contained in UL/poly [RA00].

Deciding whether a bipartite graph has a perfect matching is hard for NL [KUW86].

NL can be defined in a logical formalism as SO(krom) and also as FO(tc), reachability in directed graph is NL-Complete under FO-reduction.

More about...


SO[TC]: Second-Order logic with transitive closure

SO[TC] is to SO as FO[TC] is to FO. The TC operator can now also take second-order variable as argument.

In Descriptive complexity we can see thatSO[TC] is equal to PSPACE.

More about...