Disjunctive logic programs, answer sets, and the cut rule (Q2085572)

The paper deals with disjunctive logic programs with classical negation. Clauses of these disjunctive logic programs can have possibly empty heads, and more crucially, possible occurrences of negation in the bodies and in the heads of the rules. Disjunctions of atoms are considered in a constructive way. The semantics is proposed in terms of a classical notion of logical consequence. It is a generalisation of a semantics for negation-free disjunctive logic programs that offers a natural generalisation of the fixed-point semantics for definite logic programs. The approach introduced in the paper has a complete proof procedure based on a general form of the cut rule. The generalisation process presented here is based on a \textit{hyper-resolution (cut) rule} that involves a finite, arbitrary number of clauses as premises, unlike classical resolution rule that admits precisely two clauses as premises. The approach is further demonstrated by the way of deducing answer sets. Disjunctive logic programs of this paper are modal disjunctive sets of rules, and the least fixed point of such a set of rules \(F\) consists precisely of the disjunctions that are logical consequences of \(F\). In these programs, only classical negation is applied; to circumvent with excluded middle, the author does not introduce a weaker form of negation. Rather than expressing that either \(F\) or \(\neg F\) holds, one can express that either \(F\) or \(\neg F\) has been \textit{derived}, which is in accordance with Gödel's interpretation of intuitionistic logic in S4. To derive an answer set, the cut rule is not applied directly to a set of rules but to its closure under an operation that creates more rules, while still preserving logical validity (the created rules are logical consequences of those from which they originate). What is required is a form of program extension, which is a particular case of program transformation broadly applied in logic programs. As the author says, ``Our framework is not classical in the sense that classical logical inferences would make it possible to derive, from a fixed theory, all answer sets and nothing but answer sets. Rather, its key features are the following.'' \begin{itemize} \item It allows one to formalise a very general class of logic programs, with mechanical translations into the chosen logical language. \item It characterises semantics of interest in the form of some formulas being logical consequences of some theory \(T\), possibly together with conditions imposing that certain formulas be or be not logical consequences of \(T\). \item It is a unifying framework in that the characterisations all rely on a fixed set of underlying notions and a fixed classical notion of logical consequence (a claim that is partially supported by the work described in this paper, but more strongly so thanks to the additional work presented in other papers). \end{itemize} The proposed framework is purely classical in these three issues. First, it uses classical negation, second, it advocates the computation of logical consequences and third, it makes no reference to a preferred or minimal interpretation.