A Study Of Compatibility And Loop Formulas Of Normal Logic Programs

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 NP-complete to decide whether or not a logic program is consistent. Thus it makes sense to investigate the classes of tractable, consistent and far-range enough logic programs for which there are polynomial time algorithms to compute an answer set.To our best knowledge, call-consistent logic programs and FC-normal logic programs are two well-known 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 auto-compatible logic programs, which strictly contains the class of FC-normal 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 auto-compatible normal logic programs are revealed.(3) The complexities of credulous reasoning and skeptical reasoning of weakly auto-compatible logic programs are NP-complete and co-NP-complete respectively. The two issues for FC-normal logic programs are the same difficulty as that of weakly auto-compatible logic programs. The problem that whether or not a logic program is weakly auto-compatible is co-NP-complete.(4) Weakly auto-compatible logic programs and call-consistency logic programs are different in the sense that they are not comparable. It is the same case even restricting logic programs to be WF-irreducible.(5) Additionally, we revealed that (a) for an FC-normal logic program P, there exists the least FC-normal consistency property over P witnessing for the FC-normality of P and (b) call-consistency is equivalent to Lifschitz's order-consistency. They are decidable in polynomial time. Moreover, FC-normal logic programs are not comparable with call-consistent 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 first-order 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 first-order loop formulas captures the answer set semantics on instantiation-basis.(2) To check whether a normal logic program with variables has only a finite number of non-equivalent first-order loops is decidable in polynomial time if the maximum arity of predicates is fixed.