Disjunctive logic programs, answer sets, and the cut rule
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.
- A fixpoint semantics for disjunctive logic programs
- ASSAT: computing answer sets of a logic program by SAT solvers
- Autoepistemic logic
- Characterising equilibrium logic and nested logic programs: Reductions and complexity,
- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- Contextual hypotheses and semantics of logic programs
- Generalized disjunctive well-founded semantics for logic programs.
- Generic Tableaux for Answer Set Programming
- scientific article; zbMATH DE number 25190 (Why is no real title available?)
- scientific article; zbMATH DE number 591001 (Why is no real title available?)
- scientific article; zbMATH DE number 978240 (Why is no real title available?)
- scientific article; zbMATH DE number 1926616 (Why is no real title available?)
- Logic programming and knowledge representation---The A-Prolog perspective
- Logic programming and negation: A survey
- Logic programming as classical inference
- Logic programming with strong negation
- On the computational cost of disjunctive logic programming: Propositional case
- Semantical considerations on nonmonotonic logic
- Semantics of (disjunctive) logic programs based on partial evaluation
- Static semantics for normal and disjunctive logic programs
- Strong and explicit negation in non-monotonic reasoning and logic programming
- Super logic programs
- The Semantics of Predicate Logic as a Programming Language
- Magic sets for disjunctive Datalog programs
- On semantics and proof theory of disjunctive logic programs with classical negation
- scientific article; zbMATH DE number 1757966 (Why is no real title available?)
- Disjunctive answer set solvers via templates
- scientific article; zbMATH DE number 6747884 (Why is no real title available?)
- Logic Programming and Nonmonotonic Reasoning
- scientific article; zbMATH DE number 5043340 (Why is no real title available?)
- Logic programming as classical inference
This page was built for publication: Disjunctive logic programs, answer sets, and the cut rule
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2085572)
