If you can do Peano numbers...

Guaranteed termination isn't really if you give me enough rope to implement the Ackermann function.

Pure Datalog can't express peano up to infinity, its terms can't be functors as in Prolog. At best you could hardcode a successor relation up to a limit.