# First-Order Logic with Counting: At Least, Weak Hanf Normal Forms Always Exist and Can Be Computed!

arXiv: https://arxiv.org/abs/1703.01122 · HTML: https://mlsanity.com/paper/1703.01122/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 Mar 2017.

## Built on by (most cited first, 9 of 9)

- [The Descriptive Complexity of Graph Neural Networks](https://mlsanity.com/paper/2303.04613/) (2023)
- [Translating Regulatory Clauses into Executable Codes for Building Design Checking via Large Language Model Driven Function Matching and Composing](https://mlsanity.com/paper/2308.08728/) (2023)
- [Automatic Verification of Sound Abstractions for Generalized Planning](https://mlsanity.com/paper/2205.11898/) (2022)
- [Are Targeted Messages More Effective?](https://mlsanity.com/paper/2403.06817/) (2024)
- [Abstracting Situation Calculus Action Theories](https://mlsanity.com/paper/2410.14712/) (2024)
- [An Automatic Sound and Complete Abstraction Method for Generalized Planning with Baggable Types](https://mlsanity.com/paper/2501.15249/) (2025)
- [Query Languages for Machine-Learning Models](https://mlsanity.com/paper/2601.09381/) (2026)
- [Abstraction Generation for Generalized Planning with Pretrained Large Language Models](https://mlsanity.com/paper/2602.10485/) (2026)
- [Neuro-Relational Programs: Unifying Queries and Neural Computation over Structured Data](https://mlsanity.com/paper/2606.11946/) (2026)

## Abstract (arXiv)

We introduce the logic FOCN(P) which extends first-order logic by counting and by numerical predicates from a set P, and which can be viewed as a natural generalisation of various counting logics that have been studied in the literature. We obtain a locality result showing that every FOCN(P)-formula can be transformed into a formula in Hanf normal form that is equivalent on all finite structures of degree at most d. A formula is in Hanf normal form if it is a Boolean combination of formulas describing the neighbourhood around its tuple of free variables and arithmetic sentences with predicates from P over atomic statements describing the number of realisations of a type with a single centre. The transformation into Hanf normal form can be achieved in time elementary in d and the size of the input formula. From this locality result, we infer the following applications: (*) The Hanf-locality rank of first-order formulas of bounded quantifier alternation depth only grows polynomially with the formula size. (*) The model checking problem for the fragment FOC(P) of FOCN(P) on structures of bounded degree is fixed-parameter tractable (with elementary parameter dependence). (*) The query evaluation problem for fixed queries from FOC(P) over fully dynamic databases of degree at most d can be solved efficiently: there is a dynamic algorithm that can enumerate the tuples in the query result with constant delay, and that allows to compute the size of the query result and to test if a given tuple belongs to the query result within constant time after every database update.