Total and Partial Well-Founded Datalog Coincide

Jörg Flum, Bertram Ludäscher, Max Kubierschky

We show that the expressive power of well-founded Datalog does not decrease when restricted to total programs (it is known to decrease from $\Pi_1^1$ to $\Delta_1^1$ on infinite Herbrand structures) thereby affirmatively answering an open question posed by Abiteboul, Hull, and Vianu [AHV95]. In particular, we show that for every well-founded Datalog program there exists an equivalent total program whose only recursive rule is of the form where move is definable by a quantifier-free first-order formula. This yields a nice new normal form for well-founded Datalog and implies that it is sufficient to consider draw-free games in order to evaluate arbitrary Datalog programs under the well-founded semantics.

[PDF File] [PS File] [PS Slides of the talk]