Logics with Rank Operators

—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 r...

• Type: Conference
• Year: 2009
• Where: LICS
• Authors: Anuj Dawar, Martin Grohe, Bjarki Holm, Bastian Laubner
• Keywords: Computer Science, LICS 2009, Logics, Rank Operators, fixed-point Logic