We consider the problems of equivalence, satisfiability and query-reachability for datalog programs with negation and dense-order constraints. These problems are important for optimizing datalog programs. We show that both query-reachability and satisfiability are decidable for programs with stratified negation provided that negation is applied only to EDB predicates or that all EDB predicates are unary. In the latter case, we show that equivalence is also decidable. The algorithms we present are also used to push constraints from a given query to the EDB predicates. Finally, we show that satisfiability is undecidable for datalog programs with unary IDB predicates, stratified negation and the interpreted predicate ≠

(i) SLG resolution is a partial deduction procedure, consisting of several transformations. Each query is transformed step by step into a set of answer clauses; (ii) SLG resolution is sound and ideally complete for all non-floundering queries with respect to all three-valued stable models (including the well founded partial model); (iii) SLG resolution allows an arbitrary computation rule and an arbitrary control strategy for selecting transformations to apply; (iv) SLG resolution avoids both positive and negative loops and always terminates for programs with the bounded-term-size property; (v) SLG resolution has a polynomial time data complexity for well founded negation.