Omega-restricted logic programs

Abstract

We define a new syntactic class of logic programs, omega-restricted programs. We divide the predicate symbols of a logic program into two parts: domain and non-domain predicates, where the domain predicates are defined by the maximal stratifiable subset of the rules of the program. We extend the usual definition of stratification by adding a special omega-stratum that holds all unstratifiable predicates of the program. We demand that all variables that occur in a rule also occur in the rule body in a positive literal that is on a lower stratum than rule head. This restriction is syntactic and can be checked efficiently. The existence of a stable model of an omega-restricted program is decidable even when function symbols are allowed. We prove that the problem is 2-NEXP-complete and identify subclasses of omega-restricted programs such that the problem stays in NEXP or NP. The class of omega-restricted programs is implemented in the SMODELS system. © Springer-Verlag Berlin Heidelberg 2001.