Testing logic programs for local stratification

AbstractLocally stratified programs are a significant class of logic programs with negation for which both declarative and fixpoint semantics are well defined. Unfortunately in most cases recognizing local stratification is so hard a task that it has been conjectured that the problem is undecidable. Indeed, in this paper a formal proof of this undecidability is presented and rather general sufficient conditions for local stratification are introduced