Negation as Failure

Treat a ground goal's finite, exhaustive proof failure under a declared logic program and search semantics as defeasible support for weak default negation, while preserving nonmonotonicity, nontermination, floundering, and classical-negation boundaries.

Version

v3 · 2026-09-06 · History

Domain-specific #

2358

Origin domain

computer science

Subdomain

logic programming and nonmonotonic reasoning

Aliases

NAF, Negation by failure, Finite failure negation

Core Idea

Negation as Failure (NAF) is a nonmonotonic inference rule in logic programming that lets not p succeed when a proof attempt for p finitely and exhaustively fails relative to a declared program and operational semantics. Its conclusion is weak or default negation—roughly “p is not derivable here”—not automatically the classical proposition ¬p. The rule turns absence of a successful derivation into a usable, defeasible assumption only when the search has the right scope and termination properties.

For a program \(P\) and a suitably ground goal \(A\), the operational core is.

Scope of Application

NAF is native to logic programming and closely related rule-based systems.

• Prolog execution. \+ Goal provides a semidet control test that succeeds when the called goal cannot be proven by the current execution.
• Normal logic programs. Negative literals in rule bodies allow defaults and exceptions, with semantics supplied by completion, stratification, stable models, well-founded models, or related frameworks.
• Deductive databases and Datalog variants. A closed predicate with finite data and terminating rules can use non-derivability to answer negative queries or guard derived relations.
• Knowledge representation. Defaults such as “normally birds fly unless abnormal” use NAF to represent defeasible absence of an exception.
• Answer-set and extended logic programming. Default negation coexists with explicit strong negation, but the chosen stable-model or answer-set semantics—not Prolog's depth-first behavior alone—determines accepted models.
• Rule engines and policy systems. Negative guards can enable a rule when no exception, prohibition, or higher-priority condition is derivable, provided the guarded predicate is closed and evaluation terminates.

Clarity

Four outcomes must be distinguished for a goal \(p\):

1. Success: at least one derivation of \(p\) succeeds, so not p fails.
2. Finite failure: every relevant derivation branch closes without success, so not p succeeds.
3. Divergence: evaluation does not terminate, so neither \(p\) nor not p receives a finite operational answer.
4. Error or pruned search: the system stops for a reason that does not certify failure, so NAF is not licensed without an explicit semantics that reclassifies the event.

Manages Complexity

NAF lets a rule system represent exceptions without enumerating every negative fact. In a finite personnel database, for example, it is often cheaper to store suspended(alex) for exceptional cases and use not suspended(User) as a guard than to maintain an explicit not_suspended fact for every ordinary account. The rule compresses a potentially large negative extension into a proof-failure test.

Abstract Reasoning

NAF changes the logic of information growth. In a monotonic system, if \(P\vdash q\), then \(P\cup P'\vdash q\). With NAF, a conclusion can depend on \(\operatorname{not}p\), and adding a proof of \(p\) defeats that support. If

\[ \mathrm{flies}(x) \leftarrow \mathrm{bird}(x)\land \operatorname{not}\,\mathrm{abnormal}(x), \]

Knowledge Transfer

Within logic programming, the mechanism transfers literally across Prolog, deductive databases, normal logic programs, rule engines, and nonmonotonic knowledge systems: attempt the positive goal, distinguish finite failure from other outcomes, and use that failure as default-negative support under a declared semantics.

Outside formal rule systems, “absence of evidence is evidence of absence” resembles NAF only when the search or observation process is complete for the target. A warehouse may infer “no pallet in this bay” from a full scan; a clinician cannot infer “no disease” from an incomplete test panel.

Relationships to Other Abstractions

Current abstraction Negation as Failure Domain-specific

Parents (1) — more general patterns this builds on

• Negation as Failure presupposes Formal System Prime

  Negation as Failure presupposes Formal System. Its program, goal language, derivation rules, and operational semantics must be specified before proof failure has a determinate meaning.

Hierarchy paths (2) — routes to 2 parentless roots

• Negation as Failure → Formal System → Formalization → Representation → Abstraction

Show alternative path (1)

Neighborhood in Abstraction Space

Negation as Failure sits in a sparse region of the domain-specific corpus (62^nd percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Automata, Model Checking & Formal Semantics (10 abstractions)

Nearest neighbors

• Rice's Theorem — 0.88
• Formal Theory — 0.88
• Natural Number — 0.86
• Type Inference — 0.86
• Halting Problem — 0.85

Computed from structural-signature embeddings · 2026-09-08