Descriptive Complexity Of Linear Equation Systems And Applications To Propositional Proof Complexity
2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS)(2017)
摘要
We prove that the solvability of systems of linear equations and related linear algebraic properties are definable in a fragment of fixed-point logic with counting that only allows polylogarithmically many iterations of the fixed-point operators. This enables us to separate the descriptive complexity of solving linear equations from full fixed-point logic with counting by logical means. As an application of these results, we separate an extension of first-order logic with a rank operator from fixed-point logic with counting, solving an open problem due to Holm [21].We then draw a connection from this work in descriptive complexity theory to graph isomorphism testing and propositional proof complexity. Answering an open question from [7], we separate the strength of certain algebraic graph-isomorphism tests. This result can also be phrased as a separation of the algebraic propositional proof systems "Nullstellensatz" and "monomial PC".
更多查看译文
关键词
linear equations systems,linear algebraic properties,fixed-point logic,fixed-point operators,descriptive complexity,first-order logic,rank operator,descriptive complexity theory,algebraic graph-isomorphism tests,algebraic propositional proof systems,propositional proof complexity,Nullstellensatz,monomial PC
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络