Title :
Logics with Rank Operators
Author :
Dawar, Anuj ; Grohe, Martin ; Holm, Bjarki ; Laubner, Bastian
Author_Institution :
Univ. of Cambridge, Cambridge, UK
Abstract :
We introduce extensions of first-order logic (FO) and fixed-point logic (FP) with operators that compute the rank of a definable matrix. These operators are generalizations of the counting operations in FP+C (i.e. fixed-point logic with counting) that allow us to count the dimension of a definable vector space, rather than just count the cardinality of a definable set. The logics we define have data complexity contained in polynomial time and all known examples of polynomial time queries that are not definable in FP+C are definable in FP+rk, the extension of FP with rank operators. For each prime number p and each positive integer n, we have rank operators rkp for determining the rank of a matrix over the finite field GFp defined by a formula over n-tuples. We compare the expressive power of the logics obtained by varying the values p and n can take. In particular, we show that increasing the arity of the operators yields an infinite hierarchy of expressive power. The rank operators are surprisingly expressive, even in the absence of fixed-point operators. We show that FO+rkp can define deterministic and symmetric transitive closure. This allows us to show that, on ordered structures, FO+rkp captures the complexity class MODp L, for all prime values of p.
Keywords :
formal logic; polynomial matrices; counting operations; data complexity; definable matrix; definable vector space; first-order logic; fixed-point logic; fixed-point operators; matrix rank determination; polynomial time queries; rank operators; Computer science; Databases; Equations; Galois fields; Linear algebra; Logic; Pathology; Polynomials; Transmission line matrix methods; Tree graphs;
Conference_Titel :
Logic In Computer Science, 2009. LICS '09. 24th Annual IEEE Symposium on
Conference_Location :
Los Angeles, CA
Print_ISBN :
978-0-7695-3746-7
DOI :
10.1109/LICS.2009.24