Complexity of computing with extended propositional logic programs

In this paper we introduce the notion of an F-program, where F is a collection of formulas. We then study the complexity of computing with F-programs. F-programs can be regarded as a generalization of standard logic programs. Clauses (or rules) of F-programs are built of formulas from F. In particular, formulas other than atoms are allowed as "building blocks" of F-program rules. Typical examples of F are the set of all atoms (in which case the class of ordinary logic programs is obtained), the set of all literals (in this case, we get the class of logic programs with classical negation [9]), the set of all Horn clauses, the set of all clauses, the set of all clauses with at most two literals, the set of all clauses with at least three literals, etc. The notions of minimal and stable models [16, 1, 7] of a logic program have natural generalizations to the case of F-programs. The resulting notions are called in this paper minimal and stable answer sets. We study the complexity of reasoning involving these notions. In particular, we establish the complexity of determining the existence of a stable answer set, and the complexity of determining the membership of a formula in some (or all) stable answer sets. We study the complexity of the existence of minimal answer sets, and that of determining the membership of a formula in all minimal answer sets. We also list several open problems.