VERIFYING LOCAL STRATIFIABILITY OF LOGIC PROGRAMS AND DATABASES

In this paper, we deal with the problem of verifying local stratifiability of logic programs and databases presented by Przymusinski. The notion of dependency graphs is generalized from representing priority relation between predicate symbols to representing the priority between atoms. Necessary and sufficient conditions for the local stratifiability of logic programs are presented and algorithms for performing the verification are developed. Finally, we prove that a database DB containing clauses with disjunctive consequents can easily be converted into a logic program P such that DB is locally stratified iff P is locally stratified.