Depth-bounded bottom-up evaluation of logic programs

We present here a depth-bounded bottom-up evaluation algorithm for logic programs. We show that it is sound, complete, and terminating for finite-answer queries if the programs are syntactically restricted to DatalognS, a class of logic programs with limited function symbols. DatalognS is an extension of Datalog capable of representing infinite phenomena. Predicates in DatalognS can have arbitrary unary and limited n-ary function symbols in one distinguished argument. We precisely characterize the computational complexity of depth-bounded evaluation for DatalognS and compare depth-bounded evaluation with other evaluation methods, top-down and Magic Sets among others. We also show that universal safety (finiteness of query answers for any database) is decidable for DatalognS.