A Study of Compatibility and Loop Formulas of Normal Logic Programs 

Author  WangYiSong 
Tutor  ZhangMingYi;LinFangZhen 
School  Guizhou University 
Course  Computer Software and Theory 
Keywords  Logic programming answer sets consistency compatibility loop formulas 
CLC  TP311.11 
Type  PhD thesis 
Year  2007 
Downloads  94 
Quotes  2 
An arbitrary (normal) logic program possibly has one answer set, more than one answer set or no answer set at all. A logic program is consistent (or coherent) if it has at least one answer set. If there is a polynomial time algorithm to compute an answer set of a given logic program then we say that it is tractable. Generally, it is NPcomplete to decide whether or not a logic program is consistent. Thus it makes sense to investigate the classes of tractable, consistent and farrange enough logic programs for which there are polynomial time algorithms to compute an answer set.To our best knowledge, callconsistent logic programs and FCnormal logic programs are two wellknown subclasses of consistent logic programs which are tractable. Is there any other logic programs that are tractable and consistent?We propose a class of consistent logic programs—weakly autocompatible logic programs, which strictly contains the class of FCnormal logic programs. And there is a polynomial time algorithm to compute an answer set of a logic program in the category. The following results are established:(1) According to our notions of compatibility and A operator, a sufficient and necessary condition for consistency of normal logic programs is obtained.(2) Two essential characterizations of weakly autocompatible normal logic programs are revealed.(3) The complexities of credulous reasoning and skeptical reasoning of weakly autocompatible logic programs are NPcomplete and coNPcomplete respectively. The two issues for FCnormal logic programs are the same difficulty as that of weakly autocompatible logic programs. The problem that whether or not a logic program is weakly autocompatible is coNPcomplete.(4) Weakly autocompatible logic programs and callconsistency logic programs are different in the sense that they are not comparable. It is the same case even restricting logic programs to be WFirreducible.(5) Additionally, we revealed that (a) for an FCnormal logic program P, there exists the least FCnormal consistency property over P witnessing for the FCnormality of P and (b) callconsistency is equivalent to Lifschitz’s orderconsistency. They are decidable in polynomial time. Moreover, FCnormal logic programs are not comparable with callconsistent logic programs yet.ASSAT evaluates answer sets of a logic program by resorting to SAT solvers. The basic notions are loops and loop formulas of a logic program which initiated an alternative methodology to evaluate answer sets of a logic program. It is to transform a logic program to a prepositional theory such that the models of the resulted prepositional theory exactly correspond to the answer sets of the original logic program. These notions have been extended to disjunctive logic programs, logic programs with nested expressions and circumscription. A newfangled idea is to extend them from prepositional case to firstorder case, i.e., allowing variables to appear in loops and then also loop formulas. We initially set up these notions and obtain the following results:(1) Together with Clark’s completion, our notion of firstorder loop formulas captures the answer set semantics on instantiationbasis.(2) To check whether a normal logic program with variables has only a finite number of nonequivalent firstorder loops is decidable in polynomial time if the maximum arity of predicates is fixed.