TLDR
- A default is not an ordinary implication. It may add a conclusion only when a prerequisite is believed and specified justifications remain consistent with the completed belief set.
- An extension is a self-supporting completion. The candidate belief set controls which defaults are applicable, and the applicable defaults must generate that same set.
- More than one extension may be legitimate. Conflicting defaults can sustain alternative coherent views; some unrestricted theories have no extension at all.
- Normal defaults have strong structure. Reiter proves extension existence, semi-monotonicity and orthogonality for defaults whose justification is also their consequent.
- Proofs carry assumptions. Top-down default proofs track the defaults used, test their joint consistency and expose when new facts require belief revision.
Incomplete worlds invite conclusions that ordinary implication cannot safely express
A knowledge base rarely states everything that matters. People still conclude that a bird flies, that an unchanged property persists after an action, or that an unrecorded database tuple is false. Reiter’s problem is to make such moves explicit without pretending they are exceptionless laws.
An ordinary implication, Bird(x) → Flies(x), has no escape hatch. Once Tweety is known to be a bird, flight follows even after Tweety is identified as a penguin. Replacing the implication with a statistical phrase such as “most birds fly” does not by itself tell a theorem prover what it may conclude about this individual. Reiter instead treats the inference policy as a meta-rule whose use depends on the current state of belief.
The canonical reading is conditional permission. If α is believed, and each βᵢ may consistently be believed, then γ may be believed. The consistency test is not a second proof of βᵢ. It asks whether the completed belief set contains ¬βᵢ. Absence of a refutation is therefore operationally relevant, but only at a marked point in the rule.
This creates non-monotonicity. Add Bird(Tweety), fire a suitable default, and derive Flies(Tweety). Add information that contradicts the relevant justification and that conclusion may disappear. Classical consequence inside a fixed premise set remains monotonic; it is the changing applicability of defaults that makes the overall reasoning non-monotonic.
Reiter begins from examples already pressing on artificial intelligence in 1980: exceptions, frame descriptions, incomplete records, defaults in frame languages and the closed-world assumption used in databases. His logic does not collapse them into one empirical claim about frequencies. It supplies a common inferential form for drawing defeasible conclusions from incomplete descriptions.
Worked example 1 · a bird is not a law
Start with Bird(Tweety) and the normal default Bird(x):M Flies(x)/Flies(x). A compatible extension contains Flies(Tweety). If ¬Flies(Tweety) enters the facts, the default is defeated because its justification can no longer be consistently believed. The new extension retains the fact that Tweety is a bird and does not add flight.
Causal probe 1 · replace the default with material implication
With Bird → Flies, adding ¬Flies produces inconsistency rather than blocking the rule. The contrast isolates Reiter’s contribution: the condition governing use is part of the representation, not an informal instruction to the operator.
Prerequisite, justification and consequent play different roles
A default has the form α : Mβ₁,…,Mβₘ / γ. Its numerator records what must already be supported and what must remain compatible; its denominator records the conclusion licensed by that combination.
The prerequisite α is positive support. The current construction must derive it before the default contributes anything. Each justification βᵢ is checked negatively against the candidate extension: ¬βᵢ must not be present. The consequent γ is then added to the next stage of construction and ordinary first-order consequence closes the result.
The symbol M is best read here as “it is consistent to believe”. Reiter deliberately keeps extensions in first-order logic rather than putting modal formulae inside them. Defaults operate as meta-rules that complete an incomplete first-order theory. Later comparisons with autoepistemic logic are illuminating, but they should not erase this explicit design choice in the 1980 paper.
A rule may contain several justifications and a consequent unlike any of them. This generality can model a permission whose supporting assumptions differ from its output. It also creates pathologies: an arbitrary default theory may have no extension. The normal subclass aligns a single justification with the consequent, α:Mω/ω, and gains much better structural properties.
Open defaults contain variables, as almost every natural example does. Reiter first develops the machinery for closed formulae, then grounds the open theory after Skolemisation. This sequencing matters. The apparently simple Bird(x) rule becomes a countable family of closed instances over the individuals named or introduced by the theory.
apply relative to candidate E when: α is generated and ¬β₁,…,¬βₘ are absent from E
normal default: α : Mω / ω
Worked example 2 · the closed-world default
For a database relation R, :M¬R(a)/¬R(a) has no prerequisite. If R(a) cannot be derived, ¬R(a) is consistent with the candidate extension and may be added. This formalises one version of “not recorded, therefore false” while showing exactly where later positive information can defeat the conclusion.
Causal probe 2 · confuse “not proved” with “proved false”
Before the default fires, failure to derive R(a) is only absence. The default converts that absence into an explicit negative belief. Keeping those stages separate prevents a closed-world convention from masquerading as classical logic.
W states the world; D states defeasible ways to complete it
Reiter packages a knowledge base as Δ=(D,W). W is a set of closed first-order formulae. D is a set of defaults. Their separation makes the status of every conclusion inspectable.
W contains hard information: observations, definitions and constraints. It is not assumed complete. D contains policies for filling gaps. An extension must contain W, must be closed under first-order consequence and must contain the consequents of defaults applicable relative to itself.
The distinction is not simply “facts versus rules”. Ordinary implications may live in W because they are strict. A default lives in D because its application depends on consistency rather than truth-functional implication alone. The same surface sentence can be represented on either side only by changing its force.
This architecture clarifies provenance. A conclusion may be strictly entailed by W or may rest on one or more generating defaults. Reiter later uses the set of generating defaults to reconstruct an extension as the deductive closure of W together with their consequents. That support set becomes essential for proof search and belief revision.
It also clarifies update. Adding a fact to W can defeat a justification and retract a derived belief. Adding a normal default to D behaves differently: semi-monotonicity guarantees that each old extension can be enlarged to some extension of the augmented theory. The logic is therefore non-monotonic in information while enjoying a restricted monotonicity in normal default rules.
Worked example 3 · persistence as a frame default
If Open(door,s) holds before an action f, a normal frame default can propose Open(door,f(s)) provided that continued openness is consistent. An explicit effect that closes the door blocks the persistence conclusion. The default does not enumerate every action that leaves the door untouched.
Causal probe 3 · move the frame default into W
Turning persistence into a strict implication makes exceptional actions inconsistent with the theory. Leaving it in D states the intended asymmetry: persistence is assumed until an effect supplies contrary information.
A candidate is acceptable only when it generates itself
The defining difficulty is circular but precise. To know which defaults fire, one must know the final beliefs. To know the final beliefs, one must know which defaults fire. Reiter resolves the circle with an operator Γ and asks for fixed points.
For a proposed set S, Γ(S) is the smallest set containing W, closed under first-order consequence, and closed under every default whose prerequisite is generated and whose justifications are consistent with S. S is an extension exactly when Γ(S)=S.
The stage construction makes the two time scales visible. E₀=W. At stage i+1, take the classical closure of Eᵢ and add consequents whose prerequisites occur in Eᵢ, while checking justification negations against the final candidate E. The union of all stages must equal E. Candidate beliefs therefore cannot be inserted merely to make themselves convenient; they must be generated from W and applicable defaults.
Extensions are minimal in a strong sense: if E and F are extensions of the same closed theory and E⊆F, then E=F. One cannot take a legitimate extension and pad it with unsupported beliefs while retaining extension status. Yet minimality does not guarantee uniqueness. Two extensions may be incomparable.
Generating defaults supply a second characterisation. Once E is known, collect defaults whose prerequisites are in E and whose justification negations are absent. E is exactly the first-order closure of W plus their consequents. The extension is thus a coherent package of conclusions and the defeasible commitments that generate them.
Worked example 4 · a self-defeating default
Let W be empty and D contain :M¬A/A. Suppose A is absent from the candidate. Then ¬A is consistent and the default generates A. Suppose A is present. Then the justification ¬A is blocked and A is not generated. Neither candidate reproduces itself, so the theory has no extension.
Causal probe 4 · accept any consistent completion
Both arbitrary additions and circular wishes would pass. Γ(E)=E demands grounded generation as well as compatibility. It is the difference between a coherent story one can invent and a completion licensed by the theory.
Conflicting defaults can create several coherent views
An incomplete theory need not dictate one extension. Reiter treats each extension as an acceptable set of beliefs about the described world. The logic itself does not always select among them.
Consider the later-famous Nixon diamond. Nixon is a Quaker and a Republican. A normal default says Quakers are pacifists; another says Republicans are not pacifists. One extension applies the first and blocks the second. Another applies the second and blocks the first. Neither contains the other.
This is not classical inconsistency. Each extension is internally coherent. The conflict occurs between possible completions. For closed normal theories, Reiter’s orthogonality theorem says that the union of two distinct extensions is inconsistent. They disagree sharply enough that some formula appears positively in one and negatively in the other.
Later literature commonly distinguishes credulous conclusions, which occur in at least one extension, from sceptical conclusions, which occur in every extension. Reiter’s 1980 proof theory deliberately targets what he calls believability: whether some extension contains β. He explicitly declines to make the intersection of all extensions the paper’s theoremhood target.
That historical choice matters when describing an agent. An implementation may maintain one task-conditioned extension, expose all alternatives, or restrict actions to their intersection. Those are policies above the base semantics. Calling the intersection “what Reiter’s agent believes” would overwrite his stated view that reasoning proceeds within one coherent extension until evidence forces revision.
Worked example 5 · a penguin default does not automatically outrank a bird default
If Bird(Opus), Penguin(Opus), Bird:M Flies/Flies and Penguin:M¬Flies/¬Flies are all present, specificity alone is not a selection rule in Reiter’s semantics. The theory can have a flying extension and a non-flying extension. A modeller must encode an exception condition or add a separate priority formalism if one answer is intended.
Causal probe 5 · merge the extensions
The union contains Pacifist(N) and ¬Pacifist(N), violating consistency. The intersection is safe but withholds both. Choosing one, merging all and intersecting all are different decisions with different informational and action consequences.
Aligning justification and conclusion buys existence, locality and separation
A normal default has form α:Mω/ω. Reiter calls the class both natural and technically fortunate. The restriction rules out the self-defeating pattern and supports three major results.
First, every closed normal default theory has an extension. If W is inconsistent, the unique inconsistent extension contains every closed formula. If W is consistent, Reiter constructs a consistent extension by selecting maximal compatible normal consequents stage by stage.
Second, normal theories are semi-monotonic in their defaults. If D′⊆D and E′ is an extension of (D′,W), then some extension E of (D,W) contains E′ and preserves its generating defaults. Adding normal default rules can create or extend alternatives, but it need not destroy the old completion’s beliefs.
Third, distinct extensions are orthogonal: their union is inconsistent. The first stage at which their constructions diverge must add a normal consequent ω on one side while the other side contains ¬ω. This makes multiplicity a genuine conflict among belief packages, not a harmless difference in unsupported decoration.
These results support local proof search. Because an extension built from a subset of normal defaults can be extended after more normal defaults are restored, a proof need not inspect every default in the knowledge base. It still requires a global consistency check against W. Locality with respect to D does not become locality with respect to the world theory.
Worked example 6 · adding a normal default
Suppose a theory has an extension in which Ava is believed to be at home. Add a normal default about typical office hours. Semi-monotonicity says there is some extension of the enlarged theory that preserves the old extension. It does not say every new extension preserves it, nor that adding new facts has the same benign effect.
Causal probe 6 · add a fact instead of a default
A new observation can contradict a prior justification and force retraction. The asymmetry is a useful model audit: “we added knowledge” is too coarse. Ask whether the update changed W or enlarged D, and whether the defaults are normal.
Believability becomes a finite support chain plus a consistency obligation
For a consistent closed normal theory, β belongs to some extension exactly when β has a default proof. The proof is not an ordinary derivation with hidden defeasible steps. It explicitly records finite sets of defaults and validates their joint consequences.
A default proof is a finite sequence D₀,…,Dₖ. W plus the consequents of D₀ must entail the target β. At each later level, W plus the consequents of Dᵢ must entail the prerequisites of the defaults in Dᵢ₋₁. The last set Dₖ is empty, so the chain bottoms out in W.
One more condition prevents the support chain from licensing contradiction: W together with the consequents of every default used across the proof must be satisfiable. Reiter calls the union of these defaults the proof’s default support. That set is a compact account of which assumptions made the belief possible.
The result is sound and complete for believability in consistent closed normal theories. If the finite conditions hold, semi-monotonicity extends the local construction to the full theory. Conversely, every formula in an extension has a proof supported by generating defaults of that extension.
There is a hard computational boundary. For unrestricted first-order normal default theories, the extension membership problem is not even semi-decidable. The satisfiability condition is not an awkward removable detail. It reflects the impossibility of enumerating all satisfiable first-order formulae. Reiter concludes that computational treatments require heuristic components and may sometimes form mistaken beliefs.
Worked example 7 · support is part of the answer
A query “Does the vehicle remain operational?” may be proved from a persistence default and a normal-condition default. Returning only “yes” hides the conditions under which yes was licensed. Returning the default support lets a later fault observation identify exactly which derived beliefs are threatened.
Causal probe 7 · delete the satisfiability test
One can assemble a chain whose defaults jointly conclude P and ¬P. Each local prerequisite may be provable, yet the package is not a coherent extension. Local reachability is insufficient without global compatibility.
The query can select relevant defaults without making the world theory local
Reiter refines the abstract proof conditions into top-down default proofs that interface with linear resolution. The target drives clause selection; introduced consequent clauses carry the identities of the defaults that authorised them.
Begin with a linear resolution proof of β from clauses of W and clauses derived from default consequents. Every default introduced becomes an obligation: prove its prerequisite in the next resolution proof. Repeat until a proof introduces no new defaults. Then test W together with all introduced consequents for satisfiability.
This makes default use inspectable inside theorem proving. Indexed clauses carry sets of defaults through resolution. A successful top-down proof returns both the target and its assumption footprint. For consistent closed normal theories, top-down default proofs are complete for membership in some extension.
The query supplies focus. A proof for one belief can ignore defaults unrelated to that proof, a significant advantage in a large domain. Reiter notes that the search can favour default-free proofs first. Such conclusions have firmer status because adding first-order facts cannot retract them through defeated justifications.
The global boundary remains. The final consistency check includes all of W, even though only selected defaults appear. Semi-monotonicity justified locality over D; nothing comparable makes arbitrary facts irrelevant. This split between focused support search and global world consistency anticipates a recurring knowledge-representation architecture.
Worked example 8 · default-free first
For a medical knowledge base, first ask whether the observation is entailed by recorded tests and strict physiology. Only if that proof fails introduce a typical-case default. The final answer can then distinguish “strictly established” from “believable under defaults d₃ and d₇”.
Causal probe 8 · treat irrelevant defaults as free to ignore in every sense
Top-down locality applies to selecting defaults, not to deleting inconvenient facts from W. A distant-looking hard constraint can make the selected consequents inconsistent. The proof may be focused; the consistency boundary cannot be fabricated around it.
A reasoner must keep its derived beliefs inside one common extension
Reiter does not present extensions as a static catalogue only. He considers a reasoner that derives beliefs over time, reuses them as lemmas and receives new facts or defaults. The operational invariant is common-extension membership.
It is unsafe to choose one belief from extension E₁ and another from incompatible extension E₂ merely because each is individually believable. The current set B must fit inside some single extension. Reiter supplies a sufficient consistency condition based on the union of the default supports of the proofs used for B.
If the condition fails, revision is required. The paper sketches the direction rather than a complete algorithm: first try to rederive a minimal subset of beliefs so that their new proof supports are jointly consistent; failing that, reject a minimal subset. Reiter connects this role to Doyle’s truth-maintenance system.
New facts are dangerous because they may violate prior default assumptions. If W∪F together with the consequents supporting current beliefs remains consistent, an extension of the updated theory contains those beliefs. If not, the condition for retaining them is gone. The logic identifies the revision trigger even when it does not uniquely choose the repair.
New closed normal defaults are different. Semi-monotonicity gives the “comforting” result that beliefs already sharing an extension can continue to share some extension after such defaults are added. Again, this is an existential preservation claim. A system that switches to a different new extension may still change its working beliefs.
Worked example 9 · revision through a support ledger
A planning assistant believes Route A is open using a normal traffic default and believes the delivery is feasible using Route A as a lemma. A closure report defeats the traffic default. The support ledger reveals that both beliefs share the threatened assumption, so re-planning can target the affected branch instead of discarding every conclusion.
Causal probe 9 · retain beliefs one by one
Each old belief may still appear in some updated extension while no single extension contains them all. Independent retention tests can assemble an incoherent state. The invariant belongs to the package, not merely to each proposition.
Variables become grounded instances over an expanded language
The examples that motivate the paper are open defaults, yet the clean fixed-point theory begins with closed ones. Reiter bridges the gap through Skolemisation and grounding rather than leaving variable scope informal.
Existential information can introduce individuals not named by the original constants. Reiter Skolemises W and default consequents, adding functions that denote those witnesses. Ground terms constructible from the original and Skolem function symbols form the theory’s individuals.
Every open default is then instantiated over those ground terms. The result CLOSED(Δ) may contain countably many closed defaults, but the earlier theory did not assume finiteness. An extension of the open theory is defined as an extension of this grounded closed theory.
The method ensures that individuals introduced by existential facts or by defaults can participate in later default inferences. If a default supplies the existence of something satisfying P, a second open default can apply Q to that same Skolem witness, supporting an existential conclusion that something satisfies both.
Reiter then lifts the top-down proof machinery back to open defaults using standard resolution techniques. The price of expressive first-order representation remains severe: grounding can be infinite and extension membership inherits non-semi-decidability. The formal generalisation is exact, not a claim of automatic tractability.
Worked example 10 · an unnamed individual persists across defaults
Suppose W says that some individual is Q. Skolemisation names the witness c. The open default Q(x):M P(x)/P(x) produces P(c), supporting ∃x(Q(x)∧P(x)). Without a stable witness term, two existential statements could be incorrectly treated as if they concerned the same individual or could fail to connect when they should.
Causal probe 10 · ground only over original constants
An existentially introduced object disappears from the range of defaults. The resulting system is not Reiter’s general semantics and can miss conclusions the paper explicitly intends to capture.
Enumerate candidate extensions, then test whether each one generates itself
This finite propositional laboratory exposes three cases: one normal extension, two conflicting normal extensions and a non-normal theory with no extension. It exhaustively checks every consistent candidate in the displayed vocabulary.
Laboratory boundary
The engine implements exact fixed-point enumeration for the named finite literal fragment shown on screen, with explicit complements and forward closure of strict rules. It is not a general first-order default-logic prover. The three tests are exact relative to this miniature vocabulary.
Extensions formalise coherent completion, not probability, priority or guaranteed tractability
Reiter’s formal precision is easiest to appreciate when its boundaries remain visible. Default logic answers a particular question: which deductively closed belief sets reproduce themselves under consistency-conditioned rules?
It does not assign frequencies or degrees of belief. A default can represent “normally” without encoding how often the consequent is true. Nothing in extension membership alone supplies calibration, expected utility or a ranking of rare exceptions.
It does not automatically prefer the more specific default. Conflicts can generate multiple extensions. Priority variants and specificity principles developed later add selection policies, but they are extensions of the framework rather than hidden clauses in the 1980 definition.
It does not guarantee an extension for arbitrary defaults, nor a unique extension for normal ones. Normality guarantees existence and strong structure. Uniqueness follows under additional consistency conditions, not from the word normal itself.
It does not make first-order default reasoning mechanically complete in practice. The non-semi-decidability theorem is unusually candid. Any practical implementation restricts the language, accepts incomplete search, uses heuristics or translates to another decidable formalism.
Later work also reinterprets the semantics. Denecker, Marek and Truszczyński argue that Reiter’s rules are better understood as a dialect of autoepistemic reasoning, because their applicability refers to what the theory itself does and does not support. Their operator analysis connects Reiter extensions with stable fixpoints while distinguishing them from Moore expansions. This is valuable retrospective context, not vocabulary Reiter needed for his first-order presentation.
Computational complexity deepens the warning. Propositional default-logic decision problems occupy the polynomial hierarchy in general, and conflicts may generate exponentially many extensions. Syntactic fragments and priorities can change the boundary, but no single performance statement covers the formalism.
| Claim | What follows | What does not follow |
|---|---|---|
| β is in one extension | β is believable in Reiter’s proof-theoretic sense | β is in every extension |
| All defaults are normal | At least one extension exists | The extension is unique |
| D grows by normal defaults | Each old extension embeds in some new extension | Every new extension contains every old belief |
| A proof uses few defaults | Default selection can be local | The final consistency test may ignore W |
| A conclusion is sceptical | It lies in the intersection of extensions | Reiter’s 1980 proof theory adopted sceptical theoremhood |
Worked example 11 · action needs a projection policy
A diagnostic assistant finds two extensions, each supporting a different repair. Showing both is an epistemic result. Authorising a repair requires a decision rule: demand sceptical support, request more evidence, rank extensions, or attach utilities. Default logic structures the alternatives but does not supply the whole action policy.
Causal probe 11 · attach confidence to extension count
One extension is not automatically high confidence, and ten extensions are not probabilities of one tenth. Extension multiplicity records logical alternatives under a representation. It is not a calibrated sampling distribution.
Make defeasible assumptions first-class, enumerable and revisable
The durable lesson is architectural. A reasoning system should not hide “usually”, “unless”, “not known” and “still consistent” inside procedural code. It should expose the conditions that license a conclusion and retain the support needed to withdraw it.
Separate the world layer from the completion layer. Hard constraints and observations belong in W; explicitly defeasible policies belong in D. This prevents a convenient assumption from acquiring the force of a law and makes updates auditable.
Compute coherent states, not isolated answers. A belief is safe to combine with other working beliefs only when the package fits one extension. In modern terms, provenance should include the assumption set and the selected world view, not merely a chain of textual citations.
Expose ambiguity. Multiple extensions are not an exception to conceal. They are evidence that the representation underdetermines a conclusion. An interface can show shared conclusions, branch-specific conclusions and the facts that would defeat each branch.
Test fixed points. A candidate state must be regenerated from the strict base and defaults that remain applicable relative to that state. This blocks unsupported additions and self-defeating circularity. The laboratory turns that semantic criterion into three executable invariants.
Plan for revision at the moment of derivation. Record which defaults support each result. When a new fact arrives, recompute or revalidate only the threatened support packages, then check that the retained beliefs still inhabit a common extension.
Finally, state the computational envelope. Finite propositional fragments can be exhaustively tested; richer systems need restrictions and search policies. A useful production claim names the fragment, the completeness guarantee, the timeout semantics and what “unknown” means.
Worked example 12 · a bounded policy agent
An access agent knows strict identity and entitlement facts in W. D contains defaults such as “if a credential is valid and no revocation is known, treat it as active”. The agent records the credential-status default in every derived authorisation. A revocation event defeats that justification and invalidates dependent conclusions before another action is attempted.
Causal probe 12 · keep only the final decision
When contrary evidence arrives, the system cannot distinguish a strict entitlement from a default-supported one. It must either retain an unsafe decision or recompute everything. Support-aware beliefs make revision both safer and more selective.
What survived formal, historical and delivery challenge
Review one: formal fidelity and pedagogy. The reconstruction was checked against the complete 52-page primary scan: motivating examples, Definition 1, staged characterisation, minimality, generating defaults, the no-extension example, normal theories, existence, semi-monotonicity, orthogonality, default proofs, extension-membership limits, top-down resolution, belief revision, Skolemisation, grounding and lifted proofs.
The largest fidelity risk was importing a specificity winner into Reiter’s semantics. The paper does not automatically make the penguin rule defeat the bird rule. The companion therefore presents conflict as multiple extensions unless exception conditions or a later priority formalism are added. A second risk was describing the intersection as Reiter’s chosen theoremhood. He explicitly targets membership in some extension.
Review two: evidence boundaries and executable delivery. Later vocabulary, including sceptical and credulous reasoning, stable-fixpoint analysis, autoepistemic reinterpretation and propositional complexity classes, is labelled as later context. It is not projected backwards into the primary’s claims. Examples that are pedagogical rather than printed in the paper are identified by their captions and prose.
All ten figures have titles, descriptions, captions and scoped sources. Animation is redundant and disabled under reduced-motion preference. The laboratory enumerates all candidates in its finite fragment, reports zero extensions without fabricating a fallback, and checks soundness, completeness and projection. Desktop, tablet and phone layouts are release gates.
Review verdict
Pass 1: semantic and historical reconstruction: passed after preserving Reiter’s believability target, grounding method and normal-theory qualifications. Pass 2: evidence and delivery: passed after separating primary claims from later interpretations and making all extension outcomes machine-checkable.
Twelve cards for durable recall
Logic plus control now meets rules whose use depends on the completed belief state
Paper 0092 separated the meaning of an algorithm from the control that determines how its knowledge is used. Paper 0093 adds a different control boundary: a default’s consequent is available only when its prerequisite is supported and its justifications survive the candidate extension.
Kowalski’s programme asks whether different proof controls preserve a fixed logical relation. Reiter’s programme changes the object being constructed. The applicable rule set itself depends on the belief state, and several self-consistent completions may result. Search control still matters, especially in top-down default proofs, but the semantics no longer reduce to reaching one monotonic closure.
Clark’s negation as failure, Kowalski’s top-down resolution and Reiter’s consistency tests meet at a delicate interface: failure to prove can influence inference, yet loops, incompleteness and hidden assumptions cannot be treated as simple falsity. Reiter makes the assumption point syntactic and carries it into extension semantics.
Canon 0094 moves to John McCarthy’s “Circumscription — A Form of Non-Monotonic Reasoning”. Reiter completes a theory by consistency-conditioned rules; McCarthy instead minimises selected predicates so that abnormalities are as limited as the facts permit. The neighbouring papers offer two distinct formalisations of commonsense completion.
Primary source, companion scope and verification contract
This companion reconstructs Raymond Reiter’s “A Logic for Default Reasoning”, published in Artificial Intelligence, volume 13, 1980, pages 81–132, DOI 10.1016/0004-3702(80)90014-4. The primary text was checked from the complete 52-page scan, including its abstract, definitions, theorem statements, examples, proof constructions, figures, notes, references and received date. The article develops closed theory semantics, normal defaults, proof theory, top-down resolution, belief revision and the grounding of open defaults.
Verification contract. Five orientation claims, ten accessible animated SVG figures, twelve worked examples, twelve causal probes, twelve memory cards, two comprehensive reviews and three executable exact tests. The release checks British English, reduced-motion support, responsive rendering at 1440, 768 and 390 pixels, source boundaries, complete citation metadata, honest zero-extension handling and identical source/generated pages.
Primary text and scholarly context
- Reiter, R. (1980). “A Logic for Default Reasoning.” Artificial Intelligence, 13, 81–132. DOI and publisher record: 10.1016/0004-3702(80)90014-4.
- McCarthy, J. (1980). “Circumscription — A Form of Non-Monotonic Reasoning.” Artificial Intelligence, 13, 27–39. DOI: 10.1016/0004-3702(80)90011-9.
- McDermott, D., & Doyle, J. (1980). “Non-Monotonic Logic I.” Artificial Intelligence, 13, 41–72. DOI: 10.1016/0004-3702(80)90012-0.
- Doyle, J. (1979). “A Truth Maintenance System.” Artificial Intelligence, 12(3), 231–272.
- Clark, K. L. (1978). “Negation as Failure.” In H. Gallaire & J. Minker (eds.), Logic and Data Bases, 293–322.
- Kowalski, R. A., & Kuehner, D. (1971). “Linear Resolution with Selection Function.” Artificial Intelligence, 2, 227–260.
- Denecker, M., Marek, V. W., & Truszczyński, M. (2011). “Reiter’s Default Logic Is a Logic of Autoepistemic Reasoning And a Good One, Too.” arXiv:1108.3278.
- Denecker, M., Marek, V. W., & Truszczyński, M. (2000). “Uniform Semantic Treatment of Default and Autoepistemic Logics.” arXiv:cs/0002002.
- Beyersdorff, O., Meier, A., Thomas, M., & Vollmer, H. (2009). “The Complexity of Reasoning for Fragments of Default Logic.” Journal of Logic and Computation. arXiv:0808.3884.
- Rintanen, J. (1999). “Complexity of Prioritized Default Logics.” Journal of Artificial Intelligence Research, 9, 423–461. arXiv:1105.5453.