By
Marc Denecker, KU Leuven
Mirek Truszczynski, University of Kentucky, Lexington
Joost Vennekens, KU Leuven
Full PDF ARTICLE
Extended Abstract
In its origin, logic programming was understood as the Horn fragment of first order logic (FO) augmented with a procedural interpretation induced by SLD inference (Kowalski, 1974). But already in 1975, the Prolog system developed in Marseille was extended with the negation-as-failure (NAF) inference rule, to derive negative literals not A (Roussel, 1975). The problem was that this inference rule is unsound with respect to the then accepted declarative interpretation of programs as Horn theories, as such theories do not entail negative literals ¬A. On the other hand, negation-as-failure had many useful applications in which the “unsound” conclusions were intuitively justified. This was the start of an extensive research program to study this phenomenon and to formalize it in a formal semantics of logic programming under which NAF inference would be sound. This led to the main formal semantics of LP that we know today by van Emden and Kowalski (1976), Reiter (1977), Clark (1978), Apt et al. (1988), Gelfond and Lifschitz (1988), and Van Gelder et al. (1991).
Despite this work, misunderstanding, controversies and disagreements remain about the informal semantics of logic programs and the meaning of its connectives. Two main and conflicting views on logic programming have emerged: the view of a logic program as a definition, and the view of a logic program as an autoepistemic theory. The former was proposed first by Keith Clark in his work on the completion semantics (Clark, 1978). After the Clark’s completion semantics was criticized for its problems in the case of recursive programs (Harel, 1980),it was refined to the stratified semantics for the class of stratified programs (Apt et al., 1988), and to the well-founded semantics for arbitrary normal logic programs (Van Gelder et al., 1991). The autoepistemic view, resulting in the semantics of stable models, was presented first by Michael Gelfond and Vladimir Lifschitz (1988). It was developed on the basis of the autoepistemic logic by Moore (1984), who proposed it as a formal logic for expressing the knowledge of rational reflecting agents.
Ideas closely related to NAF inference appeared independently in the context of database query answering in Ray Reiter’s work on the Closed World Assumption (Reiter, 1977). In 1980, Reiter generalized the Closed World Assumption in his default logic (Reiter, 1980), which he proposed as a formalism to study comonsense reasoning. Several years later, default logic inspired a novel semantics of logic programs proposed by Bidoit and Froidevaux (1987,1991). This semantics was eventually shown to coincide with the stable model semantics (Marek and Truszczynski, 1989; Bidoit and Froidevaux, 1991). Since default logic is equivalent to the autoepistemic logic of Moore (Denecker et al., 2011), this line of research can be taken as an alternative embodiment of the autoepistemic view.
As for the informal semantics of the negation not in logic programs, many view it as a non-standard form of negation, different from classical negation. Gelfond and Lifschitz (1988) interpret not A as “A is not known” as a semantical way to reflect the fact that the NAF inference rule infers not A if A is not provable. While this is a compelling argument, it is easy to see that it is not a binding one.
Assume that a logic has the property that its theories have complete knowledge on some class of formulas α (i.e., a theory T either entails α or entails ¬α). If such logic possesses a sound and complete inference mechanism to infer T |= α, then a (finite) failure of this engine to prove α ensures that T |= ¬α. Thus, in all such cases, the negation-as-failure rule is a sound inference rule to infer classically negated formulas. Thus, to explain negation-as-failure, one can either interpret the symbol as an epistemic operator “I do not know that…”, or one can keep the standard objective interpretation of negation and explain logic programming as a logic that expresses complete knowledge.
As an aside, we note that in the early papers on the semantics of logic programming, including those by Clark (1978) and Apt et al. (1988), the term “negation-as-failure” refers exclusively to the non-standard negation-as-failure inference rule and not to the negation connective. In those papers, negation is interpreted as the classical negation. However, in the autoepistemic view of Gelfond and Lifschitz (1988) the negation cannot be treated as the classical one anymore. To stress that, researchers following the autoepistemic view started to use the term negation-as-failure also to refer to the not connective in programs.
Much of the controversy about the meaning of negation in logic programs stems from the coexistence of these two conflicting views. Perhaps one of the most confusing aspects herein is that at least to some extent, the same formal semantics can account for both views. Specifically, there is nothing in the mathematical definition of, say, the stable model semantics for logic programs that forces one to adopt either one view or the other. This means that in principle, two programmers may use the same program to compute the same output, and yet may have a completely different idea about what this program means! In order to properly address the question of negation-as-failure, it is therefore necessary to first discuss the informal semantics of a logic program.