Testing logic programs for local stratification

From MaRDI portal





Locally 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, a formal proof of this undecidability is presented and rather general sufficient conditions for local stratification are introduced. The sufficient conditions are based on an analysis of unification patterns based on a suitably defined algebra of terms.











This page was built for publication: Testing logic programs for local stratification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1199536)