Editing Descriptive complexity theory (section)

=== Second-order Horn formulae ===
In the presence of a successor function, PTIME can also be characterised by second-order Horn formulae.

SO-Horn is the set of Boolean queries definable with SO formulae in [[disjunctive normal form]] such that the first-order quantifiers are all universal and the quantifier-free part of the formula is in [[Horn clause|Horn]] form, which means that it is a big AND of OR, and in each "OR" every variable except possibly one are negated.

This class is equal to [[P (complexity)|P]] on structures with a successor function.<ref>{{Cite journal|last=Grädel|first=Erich|date=1992-07-13|title=Capturing complexity classes by fragments of second-order logic|journal=Theoretical Computer Science|language=en|volume=101|issue=1|pages=35–57|doi=10.1016/0304-3975(92)90149-A|issn=0304-3975|doi-access=free}}</ref>

Those formulae can be transformed to prenex formulas in existential second-order Horn logic.<ref name=":2" />