Editing Logic programming (section)

===Negation as failure===
{{Main|Negation as failure}}
[[Negation as failure]] (NAF), as a way of concluding that a negative condition <code>not p</code> holds by showing that the positive condition <code>p</code> fails to hold, was already a feature of early Prolog systems. The resulting extension of [[SLD resolution]] is called [[SLD resolution#SLDNF|SLDNF]]. A similar construct, called "thnot", also existed in [[Micro-Planner (programming language)|Micro-Planner]].

The logical semantics of NAF was unresolved until [[Keith Clark (computer scientist)|Keith Clark]]<ref>{{cite book |last=Clark |first=K.L. |title=Logic and Data Bases |chapter=Negation as Failure |author-link=Keith Clark (computer scientist) |date=1977 |pages=293–322 |doi=10.1007/978-1-4684-3384-5_11 |location=Boston, MA |publisher=Springer US|isbn=978-1-4684-3386-9 }}</ref> showed that, under certain natural conditions, NAF is an efficient, correct (and sometimes complete) way of reasoning with the logical consequence semantics using the [[Negation as failure#Completion semantics|''completion'']] of a logic program in first-order logic.

Completion amounts roughly to regarding the set of all the program clauses with the same predicate in the head, say:

:<code>A :-  Body<sub>1</sub>.</code>
:<code>      ...</code>
:<code>A :-  Body<sub>k</sub>.</code>

as a definition of the predicate:

:<code>A iff (Body<sub>1</sub> or ... or Body<sub>k</sub>)</code>

where <code>iff</code> means "if and only if". The completion also includes axioms of equality, which correspond to [[Unification (computer science)|unification]]. Clark showed that proofs generated by SLDNF are structurally similar to proofs generated by a natural deduction style of reasoning with the completion of the program.

Consider, for example, the following program:
<syntaxhighlight lang="prolog">
should_receive_sanction(X, punishment) :- 
    is_a_thief(X),
    not should_receive_sanction(X, rehabilitation).
    
should_receive_sanction(X, rehabilitation) :-
    is_a_thief(X),
    is_a_minor(X),
    not is_violent(X).
    
is_a_thief(tom).
  </syntaxhighlight>
Given the goal of determining whether tom should receive a sanction, the first rule succeeds in showing that tom should be punished:

<syntaxhighlight lang="prolog">
?- should_receive_sanction(tom, Sanction).
Sanction = punishment.
</syntaxhighlight>

This is because tom is a thief, and it cannot be shown that tom should be rehabilitated. It cannot be shown that tom should be rehabilitated, because it cannot be shown that tom is a minor.

If, however, we receive new information that tom is indeed a minor, the previous conclusion that tom should be punished is replaced by the new conclusion that tom should be rehabilitated:

<syntaxhighlight lang="prolog">
minor(tom).

?- should_receive_sanction(tom, Sanction).
Sanction = rehabilitation.
</syntaxhighlight>

This property of withdrawing a conclusion when new information is added, is called non-monotonicity, and it makes logic programming a [[non-monotonic logic]].

But, if we are now told that tom is violent, the conclusion that tom should be punished will be reinstated:

<syntaxhighlight lang="prolog">
violent(tom).

?- should_receive_sanction(tom, Sanction).
Sanction = punishment.
</syntaxhighlight>

The completion of this program is:

<syntaxhighlight lang="prolog">
should_receive_sanction(X, Sanction) iff 
    Sanction = punishment, is_a_thief(X), 
    not should_receive_sanction(X, rehabilitation)
 or Sanction = rehabilitation, is_a_thief(X), is_a_minor(X),
    not is_violent(X).
    
is_a_thief(X) iff X = tom.
is_a_minor(X) iff X = tom.
is_violent(X) iff X = tom.

</syntaxhighlight>
The notion of completion is closely related to [[John McCarthy (computer scientist)|John McCarthy's]] [[Circumscription (logic)|circumscription]] semantics for default reasoning,<ref>{{cite journal | last1=Gelfond |first1=M. |last2=Przymusinska |first2=H. |last3=Przymusinski |first3=T. |date=1989 |title=On the relationship between circumscription and negation as failure |journal=[[Artificial Intelligence (journal)|Artificial Intelligence]] |volume=38 |issue=1 |pages=75–94|doi=10.1016/0004-3702(89)90068-4 }}</ref> and to [[Raymond Reiter|Ray Reiter's]] [[closed world assumption]].<ref>{{cite journal |last=Shepherdson |first=J.C. |date=1984 |title=Negation as failure: a comparison of Clark's completed data base and Reiter's closed world assumption |journal=[[The Journal of Logic Programming]] |volume=1 |issue=1 |pages=51–79|doi=10.1016/0743-1066(84)90023-2 }}</ref>

The completion semantics for negation is a logical consequence semantics, for which SLDNF provides a proof-theoretic implementation. However, in the 1980s, the satisfiability semantics became more popular for logic programs with negation. In the satisfiability semantics, negation is interpreted according to the classical definition of truth in an intended or standard model of the logic program.

In the case of logic programs with negative conditions, there are two main variants of the satisfiability semantics: In the [[well-founded semantics]], the intended model of a logic program is a unique, three-valued, minimal model, which always exists. The well-founded semantics generalises the notion of [[inductive definition]] in mathematical logic.<ref>{{cite journal |last1=Denecker |first1=M. |last2=Ternovska |first2=E. |title=A logic of nonmonotone inductive definitions |journal=[[ACM Transactions on Computational Logic]] |volume=9 |issue=2 |pages=14:1–14:52 |date=2008|doi=10.1145/1342991.1342998 |s2cid=13156469 |url=https://lirias.kuleuven.be/handle/123456789/222628 |arxiv=cs/0501025 }}</ref> [[XSB|XSB Prolog]]<ref>{{cite conference |last1=Rao |first1=P. |last2=Sagonas |first2=K. |last3=Swift |first3=T. |last4=Warren |first4=D.S. |last5=Freire |first5=J. |title=XSB: A system for efficiently computing well-founded semantics |conference=Logic Programming And Nonmonotonic Reasoning: 4th International Conference, LPNMR'97 |location=Dagstuhl Castle, Germany |date=July 28–31, 1997 |pages=430–440 |publisher=Springer Berlin Heidelberg |doi=10.1007/3-540-63255-7_33}}</ref> implements the well-founded semantics using SLG resolution.<ref>{{cite journal |author1=W. Chen |author2=D. S. Warren |title=Tabled Evaluation with Delaying for General Logic Programs
|journal=[[Journal of the ACM]] |volume=43 |issue=1 |pages=20–74 |date=January 1996 |doi=10.1145/227595.227597|s2cid=7041379 |doi-access=free }}</ref>

In the alternative [[stable model semantics]], there may be no intended models or several intended models, all of which are minimal and two-valued. The stable model semantics underpins [[answer set programming]] (ASP).

Both the well-founded and stable model semantics apply to arbitrary logic programs with negation. However, both semantics coincide for [[Syntax and semantics of logic programming#Stratified negation|stratified]] logic programs. For example, the program for sanctioning thieves is (locally) stratified, and all three semantics for the program determine the same intended model:

<syntaxhighlight lang="prolog">
should_receive_sanction(tom, punishment).
is_a_thief(tom).
is_a_minor(tom).
is_violent(tom).
</syntaxhighlight>

Attempts to understand negation in logic programming have also contributed to the development of [[Argumentation framework|abstract argumentation frameworks]].<ref>{{cite journal |author=Phan Minh Dung |title=On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming, and n–person games |journal=Artificial Intelligence |volume=77 |issue= 2|pages=321–357 |year=1995 |doi=10.1016/0004-3702(94)00041-X|doi-access=free }}</ref> In an argumentation interpretation of negation, the initial argument that tom should be punished because he is a thief, is attacked by the argument that he should be rehabilitated because he is a minor. But the fact that tom is violent undermines the argument that tom should be rehabilitated and reinstates the argument that tom should be punished.