Rank Logic is Dead, Long Live Rank Logic!

Authors Erich Grädel, Wied Pakusa



PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.390.pdf
  • Filesize: 483 kB
  • 15 pages

Document Identifiers

Author Details

Erich Grädel
Wied Pakusa

Cite AsGet BibTex

Erich Grädel and Wied Pakusa. Rank Logic is Dead, Long Live Rank Logic!. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 390-404, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CSL.2015.390

Abstract

Motivated by the search for a logic for polynomial time, we study rank logic (FPR) which extends fixed-point logic with counting (FPC) by operators that determine the rank of matrices over finite fields. While FPR can express most of the known queries that separate FPC from PTIME, nearly nothing was known about the limitations of its expressive power. In our first main result we show that the extensions of FPC by rank operators over different prime fields are incomparable. This solves an open question posed by Dawar and Holm and also implies that rank logic, in its original definition with a distinct rank operator for every field, fails to capture polynomial time. In particular we show that the variant of rank logic FPR* with an operator that uniformly expresses the matrix rank over finite fields is more expressive than FPR. One important step in our proof is to consider solvability logic FPS which is the analogous extension of FPC by quantifiers which express the solvability problem for linear equation systems over finite fields. Solvability logic can easily be embedded into rank logic, but it is open whether it is a strict fragment. In our second main result we give a partial answer to this question: in the absence of counting, rank operators are strictly more expressive than solvability quantifiers.
Keywords
  • logic
  • descriptive complexity
  • polynomial time
  • rank logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. F. Abu Zaid, E. Grädel, M. Grohe, and W. Pakusa. Choiceless Polynomial Time on structures with small Abelian colour classes. In MFCS 2014, volume 8634 of Lecture Notes in Computer Science, pages 50-62. Springer, 2014. Google Scholar
  2. A. Atserias, A. Bulatov, and A. Dawar. Affine systems of equations and counting infinitary logic. Theoretical Computer Science, 410:1666-1683, 2009. Google Scholar
  3. G. Buntrock, U. Hertrampf, C. Damm, and C. Meinel. Structure and importance of logspace-mod-classes. STACS'91, pages 360-371, 1991. Google Scholar
  4. J. Cai, M. Fürer, and N. Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12(4):389-410, 1992. Google Scholar
  5. A. Dawar. The nature and power of fixed-point logic with counting. ACM SIGLOG News, pages 8-21, 2015. Google Scholar
  6. A. Dawar, E. Grädel, B. Holm, E. Kopczynski, and W. Pakusa. Definability of linear equation systems over groups and rings. Logical Methods in Computer Science, 9(4), 2013. Google Scholar
  7. A. Dawar, M. Grohe, B. Holm, and B. Laubner. Logics with Rank Operators. In LICS'09, pages 113-122. IEEE Computer Society, 2009. Google Scholar
  8. A. Dawar and B. Holm. Pebble games with algebraic rules. In Automata, Languages, and Programming, pages 251-262. Springer, 2012. Google Scholar
  9. H.-D. Ebbinghaus and J. Flum. Finite model theory. Springer-Verlag, 2nd edition, 1999. Google Scholar
  10. E. Grädel et al. Finite Model Theory and Its Applications. Springer, 2007. Google Scholar
  11. E. Grädel and W. Pakusa. Rank logic is dead, long live rank logic! CoRR, abs/1503.05423, 2015. Google Scholar
  12. M. Grohe. The quest for a logic capturing PTIME. In LICS 2008, pages 267-271, 2008. Google Scholar
  13. Y. Gurevich and S. Shelah. On finite rigid structures. The Journal of Symbolic Logic, 61(02):549-562, 1996. Google Scholar
  14. B. Holm. Descriptive complexity of linear algebra. PhD thesis, Univ. of Cambridge, 2010. Google Scholar
  15. B. Laubner. The structure of graphs and new logics for the characterization of Polynomial Time. PhD thesis, Humboldt-Universität Berlin, 2011. Google Scholar
  16. M. Otto. Bounded Variable Logics and Counting. Springer, 1997. Google Scholar
  17. W. Pakusa. Finite model theory with operators from linear algebra. Staatsexamensarbeit, RWTH Aachen University, 2010. Google Scholar
  18. J. Torán. On the hardness of graph isomorphism. SIAM Journal on Computing, 33(5):1093-1108, 2004. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail