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 Datalog_nS, a class of logic programs with limited function symbols. Datalog_nS is an extension of Datalog capable of representing infinite phenomena. Predicates in Datalog_nS 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 Datalog_nS 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 Datalog_nS.