2017/03/03 by Dietrich Kuske, Kuske, Dietrich, Nicole Schweikardt +1
Computer Science · #Advanced Database Systems and Queries #Complexity and Algorithms in Graphs #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge
paper · pdf · doi:10.48550/arxiv.1703.01122
openalex publication_date 2017/03/03 · openalex created_date 2022/09/13 · openalex updated_date 2026/07/28
We introduce the logic FOCN(P) which extends first-order logic by counting\nand by numerical predicates from a set P, and which can be viewed as a natural\ngeneralisation of various counting logics that have been studied in the\nliterature.\n We obtain a locality result showing that every FOCN(P)-formula can be\ntransformed into a formula in Hanf normal form that is equivalent on all finite\nstructures of degree at most d. A formula is in Hanf normal form if it is a\nBoolean combination of formulas describing the neighbourhood around its tuple\nof free variables and arithmetic sentences with predicates from P over atomic\nstatements describing the number of realisations of a type with a single\ncentre. The transformation into Hanf normal form can be achieved in time\nelementary in d and the size of the input formula. From this locality result,\nwe infer the following applications: (*) The Hanf-locality rank of first-order\nformulas of bounded quantifier alternation depth only grows polynomially with\nthe formula size. (*) The model checking problem for the fragment FOC(P) of\nFOCN(P) on structures of bounded degree is fixed-parameter tractable (with\nelementary parameter dependence). (*) The query evaluation problem for fixed\nqueries from FOC(P) over fully dynamic databases of degree at most d can be\nsolved efficiently: there is a dynamic algorithm that can enumerate the tuples\nin the query result with constant delay, and that allows to compute the size of\nthe query result and to test if a given tuple belongs to the query result\nwithin constant time after every database update.\n