The proof that should have failed

Worked scenario. A synthetic bank offers a service-fee waiver to customers with a verified support need and an eligible account. The policy also says that an account with an active restriction cannot receive the waiver. A small rule engine receives four facts: Asha owns account 7; account 7 is an eligible product; Asha has verified evidence, and no active restriction appears in the current data.

The engine returns waiver_candidate(asha, acct-7). Its proof trace is clean. Each premise matches a fact, the product rule fires, and the final rule concludes that Asha is a candidate. A reviewer can inspect the entire chain in seconds.

Then an operator discovers that the restrictions feed was delayed. The absence of active_hold(acct-7) did not mean that no hold existed. It meant that the system did not know. The proof was valid under a closed-world assumption that the data pipeline had never earned.

The same act of explicit modelling created both the guarantee and the failure. By writing the rule, the team made the conclusion inspectable. By leaving the meaning of absence implicit, it made a brittle boundary look like a fact. Logic did not hallucinate. It reasoned exactly within the world it had been given.

Part I

A representation chooses a world

A machine cannot put an account, a bird or a contract inside its reasoning process. It uses a surrogate. Randall Davis, Howard Shrobe and Peter Szolovits described knowledge representation as serving several roles at once: a stand-in for the world, a set of ontological commitments, a theory of permitted reasoning, a medium for efficient computation and a language for human expression.[1] These roles explain why representation is more than storing data in a convenient shape.

Consider the token acct-7. Its characters are merely syntax. A surrounding system makes it denote one account. The predicate owns(asha, acct-7) says that a relation holds between two denoted entities. An ontology says what kinds of entities may enter that relation, whether an account can have several owners, whether a legal entity counts as a customer, and whether ownership at one time implies ownership at another. A rule then licenses a new statement from statements already accepted.

Representation is selective before it is logical. The modeller decides which distinctions exist in the machine’s world. A support need may be represented as a Boolean fact, a graded assessment, an evidence object with an expiry, or an unresolved judgement. Each choice makes some questions easy and others impossible. No theorem prover can recover a distinction that the vocabulary erased.

Symbols, predicates, ontologies and rules

A symbol is a manipulable token used to stand for something else. A name such as asha may denote an individual. A class symbol such as EligibleProduct may denote a set. Symbols gain operational meaning through interpretation, data contracts, identifiers and the procedures that connect them to sources.

A predicate expresses a property or relation that can be true or false of its arguments. verified_need(asha) is unary. owns(asha, acct-7) is binary. Arity matters because owns(account) has discarded the owner, while owns(customer, account, time) preserves a temporal dimension. Predicate design is therefore a choice about what evidence a later inference can inspect.

An ontology specifies the vocabulary and commitments of a domain: classes, relations, constraints and sometimes axioms that connect them. Thomas Gruber’s formulation emphasised a common vocabulary for shared knowledge and defined an ontology as a specification of a conceptualisation.[5] An ontology is not identical to a graph database. RDF, for example, provides subject-predicate-object triples as an abstract data model, while OWL adds formally defined semantics for classes, properties and individuals.[6][8]

A rule says which conclusions follow when premises hold. In a Horn-style rule, a conjunction of positive premises implies one positive conclusion:

owns(c,a) ∧ eligible_product(a) ∧ verified_need(c) ∧ ¬active_hold(a) → waiver_candidate(c,a)

Here c ranges over customers and a over accounts. The rule changes no world state. It derives a claim inside the knowledge base. The negated premise is safe only if the system has a defensible account of what absence means.

These four layers are often collapsed. A knowledge graph may be called an ontology even when its edge labels have no formal semantics. A rule may be presented as policy even when its predicates come from an unverified model. A class hierarchy may be treated as a validation schema even though open-world ontology semantics do not require every property to be present. The result is apparent explicitness without explicit commitments.

Logic-to-ontology anatomy A cutaway from changing world state through grounding, symbols, predicates, ontology and rules to a derived claim. Four seams mark grounding, typing, closure and exception assumptions. Changing world state accounts, people, evidence, restrictions, time Grounding and source contracts which source event makes a token refer to a current entity or state? symbols asha, acct-7 predicates owns(c,a) ontology types, relations rules licensed inference derived claim with proof trace true relative to the represented world seams: reference · typing · closure · exceptions
Figure 2. Logic-to-ontology anatomy. Authored conceptual cutaway. Each layer makes a different commitment explicit; each seam can invalidate the use of an otherwise correct inference. No quantities are measured.

Thought experiment: one rule, two ontologies

Imagine two systems with identical facts and an identical rule: every employee receives building access. Both know that Mira is a contractor. The only difference is ontological. System A defines Contractor as a subclass of Employee. System B defines contractors and employees as disjoint categories.

System A derives access. System B does not. Nothing about theorem proving, data volume or model quality changed. Only the category relation changed. This is why an ontology is not decorative metadata. It determines which statements can become premises for other statements.

Now ask which system is correct. Logic cannot answer until the organisation supplies the intended meaning of “employee” for this decision. Payroll may treat contractors as non-employees. Physical security may include them within the workforce. Employment law may use another boundary. An ontology settles a question for a context; it does not discover the one true partition of reality.

The same rule produces different consequences under different ontologies Two panels share the facts Mira is a contractor and employees receive access. In the left panel contractor is inside employee, producing access. In the right panel the classes are disjoint, so access is not derived. Only the ontology changes Ontology A: contractor ⊆ employee Employee Contractor Mira access derived Ontology B: classes disjoint Employee Contractor Mira access not derived
Figure 3. Ontological commitment changes the answer before reasoning starts. Illustrative thought experiment. The facts and rule are held constant; only the class relation varies.

What a proof actually guarantees

Formal logic separates expressions from interpretations. A knowledge base K contains sentences. An interpretation M assigns denotations to names and extensions to predicates, creating one possible state of affairs in which those sentences may be true or false. A query q is entailed when it is true in every interpretation that satisfies the knowledge base:

K ⊨ q  ⇔  ∀M (M ⊨ K ⇒ M ⊨ q)

K is the set of accepted facts and axioms. q is the candidate conclusion. M ranges over interpretations. Adding a constraint to K removes interpretations that violate it. A conclusion is forced only when no remaining interpretation makes it false.

This definition is stronger and narrower than “the answer seems reasonable”. It supports a precise countermodel test: to show that K does not entail q, construct one interpretation in which every sentence in K is true and q is false. It also exposes a crucial limit. Entailment is relative to the sentences supplied. A proof does not certify that the source facts are current, that the vocabulary matches the business meaning, or that the action implied by the conclusion is authorised.

John McCarthy’s early programme of logical AI made this separation central: represent information as sentences, then use formal consequence to reason about action and change.[2] The resulting programme exposed the frame problem and, in later work, the qualification problem: a formal account must say what changes, what persists and which unmentioned conditions can defeat an action. Those are not peripheral annoyances. They are the cost of asking a finite theory to stand in for an open world.

Entailment as filtering possible worlds A large ellipse contains possible interpretations. Facts, ontology and rules progressively narrow the set. The query is entailed only if all surviving interpretations lie in the region where the query is true. A conclusion is forced when every surviving world agrees all interpretations satisfy facts satisfy ontology satisfy rules q true throughout countermodel defeats q More axioms shrink the admissible worlds. They do not prove that the intended world is among them.
Figure 4. Model-theoretic entailment is a universal claim over remaining interpretations. Conceptual figure. The nested areas are illustrative, not measured probabilities.
Part II

Logic makes consequences inspectable

The strongest practical reason to use symbolic representation is not that it resembles human thought. It is that explicit premises and consequence relations can be inspected independently. A team can ask whether a fact was asserted or derived, which rule fired, whether an ontology implies an unintended subclass, and whether a counterexample defeats the conclusion.

A proof trace converts “the system decided” into a finite claim about premises and rules. That is valuable wherever a conclusion must be challenged, regression-tested or reconstructed. It also changes debugging. A wrong answer can be localised to source grounding, category design, rule content, inference semantics or an invalid use of the conclusion.

From a fact to a consequence: match, bind, fire, repeat

Take the rule owns(c,a) ∧ eligible_product(a) → account_holder(c). The letters c and a are variables. A fact such as owns(asha, acct-7) supplies a binding, written informally as {c ↦ asha, a ↦ acct-7}. If eligible_product(acct-7) is also known, substituting those bindings into the rule head produces account_holder(asha).

A simple forward-chaining cycle has four operations. First, match each rule’s positive premises against the current fact set. Second, join compatible bindings so that repeated variables denote the same entity. Third, check any negative premise only under its declared closure contract. Fourth, instantiate the conclusion, add it if new, and attach the rule identifier plus supporting facts. The engine repeats this cycle until it reaches a fixed point, meaning that another pass adds no facts.

In a finite, positive Horn-rule fragment, this process is monotonic: every round can add facts but cannot remove them. Because only finitely many ground atoms can be formed from the declared constants and predicates, the cycle terminates. Its final set is the least fixed point licensed by the facts and rules. That gives two useful properties. The result does not depend on which eligible rule happened to fire first, and every derived atom can carry a finite ancestry back to assertions.

Those properties are conditional rather than universal. Function symbols can generate an unbounded sequence of terms. Rules that create new individuals can prevent termination. Defaults, priorities and retractions can make firing order or conflict policy consequential. An inconsistent classical theory may need isolation or a different consequence relation. The modeller therefore chooses both a vocabulary and an inference regime.

The mechanism also explains the characteristic failure. Pattern matching is exact with respect to the representation. owns will not automatically match controls; an account identifier will not become a legal entity; a missing time argument cannot be reconstructed later. This exactness is what makes the trace testable, yet it is also what turns an omitted distinction into a hard edge. Symbolic brittleness is the operational shadow of explicit matching.

Minimal worked example: the bird that retracts a conclusion

Start with two statements: Tweety is a bird; every bird flies. Classical inference derives that Tweety flies. Now add that Tweety is a penguin and every penguin does not fly. A classical, monotonic system does not retract the first conclusion merely because more information arrived. It now contains both flies(tweety) and ¬flies(tweety). Under standard classical consequence, an inconsistent theory can entail any formula, although practical systems may isolate inconsistency or use a paraconsistent logic instead.

Human default reasoning behaves differently. “Birds normally fly” is a defeasible generalisation. The more specific penguin fact defeats it. Raymond Reiter’s default logic formalised reasoning in which a conclusion may be adopted when its prerequisite holds and its justification remains consistent, then withdrawn when defeating information appears.[3]

This repair has a price. The system now needs to know which rules are defaults, which facts defeat them, how specificity works, what to do when two defaults conflict, and whether the conclusion may leave its context. The representation becomes more faithful to ordinary reasoning by making more of its exception policy explicit.

Monotonic and defeasible reasoning react differently to new information Two timelines begin with bird Tweety and the conclusion flies Tweety. After penguin Tweety is added, the monotonic path keeps the prior conclusion and adds a conflict, while the defeasible path retracts the default conclusion. One new fact, two consequence relations Monotonic Bird(Tweety) Flies derived Penguin added Flies retained conflict appears Defeasible Bird(Tweety) Flies by default Penguin added default defeated Flies withdrawn exception wins
Figure 5. Monotonicity preserves prior entailments; defeasible reasoning permits context-bound retraction. Illustrative temporal sequence. It does not compare measured accuracy.

A small inference engine that refuses unsafe absence

The executable artefact implements a deliberately small forward-chaining engine. Facts are positive atoms. Rules contain positive premises and may contain negated premises. The engine permits negation-as-failure only for predicates declared closed for the current snapshot. If a rule asks it to infer “no active hold” from an incomplete feed, it stops rather than deriving a candidate.

Forward chaining repeatedly matches rule premises against known facts and adds new conclusions until no rule can add anything. Production systems often optimise many-pattern matching with algorithms such as Rete, but an optimisation does not change the semantic contract.[11] The important design choice here is that closure is an explicit input, not a hidden convention.

Case 1: complete hold snapshot, no active hold
DERIVED
waiver_candidate(asha, acct-7) [via waiver-candidate]
  owns(asha, acct-7) [asserted]
  eligible_product(acct-7) [via eligible-product]
    account_product(acct-7, basic) [asserted]
  verified_need(asha) [asserted]
  not active_hold(acct-7) [closed-world check]

Case 2: hold feed is incomplete
BLOCKED: Rule 'waiver-candidate' uses absence of 'active_hold'
as false, but that predicate is not declared closed.

Case 3: complete snapshot contains an active hold
NOT DERIVED

The positive case earns negation because the caller asserts that the restriction predicate is complete for the snapshot. The first negative case blocks inference because unknown is not false. The second negative case has a complete snapshot containing a hold, so the rule simply does not match. The artefact turns a semantic assumption into a property the program can test.

Runnable Python: full inference engine and self-tests

Assumptions: Python 3.10 or later; no external packages; synthetic facts only; predicates used under closed-world negation are complete, extensional snapshots and are never derived by rules. Expected output is shown above. Save the code as knowledge_representation_engine.py and run python3 knowledge_representation_engine.py.

#!/usr/bin/env python3
"""A tiny forward-chaining inference engine with explicit closure checks.

The engine is deliberately small. It supports positive Horn-style premises and
negation-as-failure only over extensional predicates that the caller has
declared complete for the current snapshot. Closed predicates may be asserted
but not derived. The engine emits proof traces so every derived fact can be tied
to a rule and supporting facts.

Run with: python3 knowledge_representation_engine.py
"""

from __future__ import annotations

from dataclasses import dataclass
from typing import Dict, Iterable, Iterator, Mapping, Sequence, Tuple

Term = str
Binding = Dict[str, Term]


def is_variable(term: Term) -> bool:
    return term.startswith("?")


@dataclass(frozen=True, order=True)
class Atom:
    predicate: str
    terms: Tuple[Term, ...]
    negated: bool = False

    def __str__(self) -> str:
        prefix = "not " if self.negated else ""
        return f"{prefix}{self.predicate}({', '.join(self.terms)})"


@dataclass(frozen=True)
class Rule:
    name: str
    premises: Tuple[Atom, ...]
    conclusion: Atom


@dataclass(frozen=True)
class Proof:
    rule: str
    supports: Tuple[Atom, ...]


class UnsafeNegation(ValueError):
    """Raised when a rule treats absence as false without a closure contract."""


class KnowledgeBase:
    def __init__(
        self,
        facts: Iterable[Atom],
        closed_predicates: Iterable[str] = (),
    ) -> None:
        facts = tuple(facts)
        if any(fact.negated for fact in facts):
            raise ValueError("Store positive facts only; negation is used in rules.")
        self.facts = set(facts)
        self.closed_predicates = set(closed_predicates)
        self.proofs: Dict[Atom, Proof] = {}

    @staticmethod
    def _bind(pattern: Atom, fact: Atom, seed: Mapping[str, Term]) -> Binding | None:
        if pattern.predicate != fact.predicate or len(pattern.terms) != len(fact.terms):
            return None
        binding = dict(seed)
        for expected, actual in zip(pattern.terms, fact.terms):
            if is_variable(expected):
                previous = binding.get(expected)
                if previous is not None and previous != actual:
                    return None
                binding[expected] = actual
            elif expected != actual:
                return None
        return binding

    @staticmethod
    def _instantiate(atom: Atom, binding: Mapping[str, Term]) -> Atom:
        terms = tuple(binding.get(term, term) for term in atom.terms)
        if any(is_variable(term) for term in terms):
            raise ValueError(f"Unbound variable in {atom}")
        return Atom(atom.predicate, terms, atom.negated)

    def _positive_matches(
        self,
        premise: Atom,
        bindings: Sequence[Binding],
    ) -> Iterator[tuple[Binding, Atom]]:
        for binding in bindings:
            for fact in sorted(self.facts):
                matched = self._bind(premise, fact, binding)
                if matched is not None:
                    yield matched, fact

    def _rule_matches(self, rule: Rule) -> Iterator[tuple[Binding, Tuple[Atom, ...]]]:
        states: list[tuple[Binding, Tuple[Atom, ...]]] = [({}, ())]
        for premise in rule.premises:
            if premise.negated:
                if premise.predicate not in self.closed_predicates:
                    raise UnsafeNegation(
                        f"Rule '{rule.name}' uses absence of '{premise.predicate}' "
                        "as false, but that predicate is not declared closed."
                    )
                next_states: list[tuple[Binding, Tuple[Atom, ...]]] = []
                for binding, supports in states:
                    grounded = self._instantiate(premise, binding)
                    positive = Atom(grounded.predicate, grounded.terms)
                    if positive not in self.facts:
                        next_states.append((binding, supports + (grounded,)))
                states = next_states
                continue

            next_states = []
            for binding, supports in states:
                matches = self._positive_matches(premise, [binding])
                for matched, fact in matches:
                    next_states.append((matched, supports + (fact,)))
            states = next_states

        yield from states

    def infer(self, rules: Sequence[Rule]) -> set[Atom]:
        derived_predicates = {rule.conclusion.predicate for rule in rules}
        overlap = derived_predicates & self.closed_predicates
        if overlap:
            names = ", ".join(sorted(overlap))
            raise ValueError(
                "Closed predicates must be extensional input facts, not rule "
                f"conclusions: {names}"
            )

        changed = True
        while changed:
            changed = False
            for rule in rules:
                for binding, supports in self._rule_matches(rule):
                    conclusion = self._instantiate(rule.conclusion, binding)
                    if conclusion.negated:
                        raise ValueError("Rule conclusions must be positive atoms.")
                    if conclusion not in self.facts:
                        self.facts.add(conclusion)
                        self.proofs[conclusion] = Proof(rule.name, supports)
                        changed = True
        return set(self.facts)

    def explain(self, fact: Atom, depth: int = 0) -> str:
        indent = "  " * depth
        proof = self.proofs.get(fact)
        if proof is None:
            return f"{indent}{fact} [asserted]"
        lines = [f"{indent}{fact} [via {proof.rule}]"]
        for support in proof.supports:
            if support.negated:
                lines.append(f"{indent}  {support} [closed-world check]")
            else:
                lines.append(self.explain(support, depth + 1))
        return "\n".join(lines)


def A(predicate: str, *terms: str, negated: bool = False) -> Atom:
    return Atom(predicate, tuple(terms), negated)


RULES = (
    Rule(
        "eligible-product",
        (A("account_product", "?account", "basic"),),
        A("eligible_product", "?account"),
    ),
    Rule(
        "waiver-candidate",
        (
            A("owns", "?customer", "?account"),
            A("eligible_product", "?account"),
            A("verified_need", "?customer"),
            A("active_hold", "?account", negated=True),
        ),
        A("waiver_candidate", "?customer", "?account"),
    ),
)


def run_case(label: str, facts: Iterable[Atom], closed: Iterable[str]) -> None:
    print(f"\n{label}")
    kb = KnowledgeBase(facts, closed_predicates=closed)
    target = A("waiver_candidate", "asha", "acct-7")
    try:
        kb.infer(RULES)
    except UnsafeNegation as error:
        print(f"BLOCKED: {error}")
        return

    if target in kb.facts:
        print("DERIVED")
        print(kb.explain(target))
    else:
        print("NOT DERIVED")



def self_test() -> None:
    base = {
        A("owns", "asha", "acct-7"),
        A("account_product", "acct-7", "basic"),
        A("verified_need", "asha"),
    }
    target = A("waiver_candidate", "asha", "acct-7")

    complete = KnowledgeBase(base, closed_predicates={"active_hold"})
    assert target in complete.infer(RULES)

    held = KnowledgeBase(
        base | {A("active_hold", "acct-7")},
        closed_predicates={"active_hold"},
    )
    assert target not in held.infer(RULES)

    incomplete = KnowledgeBase(base)
    try:
        incomplete.infer(RULES)
    except UnsafeNegation:
        pass
    else:
        raise AssertionError("Incomplete predicates must block negation-as-failure")

    invalid_rules = (
        Rule(
            "derive-closed-predicate",
            (A("flagged", "?account"),),
            A("active_hold", "?account"),
        ),
    )
    invalid = KnowledgeBase(
        {A("flagged", "acct-7")},
        closed_predicates={"active_hold"},
    )
    try:
        invalid.infer(invalid_rules)
    except ValueError:
        pass
    else:
        raise AssertionError("Closed predicates must remain extensional")


def main() -> None:
    self_test()
    base = {
        A("owns", "asha", "acct-7"),
        A("account_product", "acct-7", "basic"),
        A("verified_need", "asha"),
    }

    run_case(
        "Case 1: complete hold snapshot, no active hold",
        base,
        closed={"active_hold"},
    )
    run_case(
        "Case 2: hold feed is incomplete",
        base,
        closed=set(),
    )
    run_case(
        "Case 3: complete snapshot contains an active hold",
        base | {A("active_hold", "acct-7")},
        closed={"active_hold"},
    )


if __name__ == "__main__":
    main()
A production-shaped inference separates evidence, world state, ontology, closure and output Evidence and system records flow through typed predicates. A closure gate checks whether absence may be used. Rules derive a candidate with a proof trace. The candidate remains separate from approval and execution. The symbolic layer is bounded on both sides evidence and records ownership · product · verified need · holds typed predicates identity · time · scope closure earned? unknown or stale block or gather evidence rules derive only candidate + proof trace not yet an effect decision authority review · approve · reject outside inference semantics symbolic reasoning boundary A proof can support a decision without silently acquiring authority to execute it.
Figure 6. Production-shaped symbolic inference needs explicit entry and exit boundaries. Synthetic architecture. The rule engine receives typed, scoped facts and returns a candidate claim; approval and execution remain separate.
Part III

Where explicit knowledge breaks

The usual story says symbolic systems are brittle because programmers failed to write enough rules. That diagnosis is incomplete. More rules can repair known gaps, but the deeper problem is that every usable representation commits to a vocabulary, a source connection, a treatment of absence, an exception policy and a computational fragment. The world can cross any of those boundaries.

1. Grounding: the symbol may not touch the thing

Stevan Harnad’s symbol grounding problem asks how the meanings of formal tokens could be intrinsic to a cognitive system rather than borrowed from an external interpreter.[4] That is a philosophical and cognitive problem, broader than ordinary software integration. The operational analogue is narrower: what event, sensor, record or human judgement makes active_hold(acct-7) correspond to a current restriction?

An identifier may refer to the wrong entity after a merge. A classifier may emit vulnerable_customer without a stable decision definition. A document extractor may turn a proposed clause into an asserted obligation. Logic cannot repair these errors because the bad symbol is already inside the premises. Formal validity begins after grounding; operational reliability begins before it.

2. Vocabulary: the world may need a distinction the ontology erased

A Boolean verified_need hides who verified it, for which purpose, against which evidence, under which policy version and until when. That compression may be appropriate for a short-lived rule. It becomes dangerous when the fact is reused across contexts. The modeller must decide whether to add arguments, reify the evidence as an object, or prohibit reuse.

Categories also change. “Employee”, “customer”, “default”, “material change” and “high risk” may have several legitimate definitions. An ontology can make one definition precise, but precision does not guarantee portability. The more contexts a vocabulary serves, the more likely that its apparently shared terms conceal different decision boundaries.

3. Closure: absence may mean false, unknown, delayed or inapplicable

Databases often operate under a closed-world convention: if a complete table contains no matching row, the application may treat the proposition as false. OWL uses an open-world assumption: a missing assertion may simply be unknown.[8] Neither convention is universally correct. Closure is a property of a predicate, source, scope and time, not of an entire system.

The distinction between ontology and validation matters here. OWL’s own primer warns that it is not a syntax-conformance schema and does not require a property to be explicitly present. SHACL, by contrast, is a W3C language for validating RDF graphs against stated conditions.[10] Use ontology reasoning to derive consequences across admissible interpretations. Use validation to ask whether the submitted graph has the required shape. Confusing the two produces both missed errors and false expectations.

Thought experiment: the sealed room and the street

A motion detector reports no person. In a sealed laboratory, every entrance is controlled, the detector covers the full room, its health check is current, and the snapshot is synchronous. Under those conditions, absence can support room_empty.

Move the same detector and rule to a public street. The field of view is partial, people can be occluded, the feed can lag and the scene changes during inference. The sensor reading is identical. Only the completeness boundary changed. In the street, “not detected” should remain unknown.

This thought experiment varies one causal feature: whether observation is complete for the predicate being negated. The lesson is stronger than “check data quality”. Negation is an authority claim about the boundary of observation. A system should record who may make that claim, for which scope and for how long.

4. Exceptions: ordinary rules are rarely universal

Commonsense reasoning repeatedly encounters defaults, temporal persistence, causal side effects, exceptions and context dependence. Ernest Davis’s survey of logic-based commonsense formalisations shows how broad and difficult this programme remains.[12] A rule that handles the first ten cases may fail on the eleventh because the missing qualification was never represented.

Nonmonotonic formalisms can represent defaults and retraction, but they do not abolish the modelling burden. Someone still chooses which predicates may vary, which defaults are preferred, how conflicts resolve and when an exception expires. A system that cannot explain those choices has moved brittleness into an opaque priority mechanism.

5. Expressiveness: more sayable worlds can make reasoning harder

Formal languages trade expressive power against computational properties. OWL 2 therefore defines profiles that restrict the language for different reasoning tasks. OWL 2 EL supports large class and property hierarchies with polynomial-time core reasoning; OWL 2 QL is designed for query answering over large instance data; OWL 2 RL supports rule-oriented implementations.[9]

The trade is not merely an implementation inconvenience. A 2025 preprint reports that pure minimal-model concept satisfiability is undecidable even for the lightweight description logic EL, while regaining decidability requires restrictions with substantial worst-case complexity.[13] This is one recent theoretical result, not a universal verdict on practical ontologies. It illustrates the general mechanism: adding seemingly natural ways to minimise abnormal cases can cross a formal boundary.

Failure boundary. The symbolic mechanism ceases to help when the system cannot defend stable predicate meanings, current grounding, scoped completeness for negation, bounded exception semantics or an acceptable reasoning cost. Beyond that boundary, a valid proof remains evidence about the encoded theory; it is not reliable evidence about the live world.

The symbolic failure surface rises with missingness, semantic volatility and exception density A triangular field shows a low-risk basin near stable semantics, complete facts and few exceptions. Risk rises toward three corners representing missing facts, changing categories and dense exceptions. Illustrative brittleness surface bounded symbolic fit semantic volatility missingness exception density Risk also rises when grounding is weak or the chosen logic exceeds the compute budget.
Figure 7. Explicit rules are safest in a bounded basin. The relationship is illustrative, not measured. Movement towards any corner increases the chance that valid in-system reasoning diverges from the intended world.

Serious objection: all software has assumptions

A critic may object that logic is being blamed for a universal engineering fact. Database schemas, ordinary code, neural models and human procedures also rely on incomplete categories and stale inputs. That objection is correct. Symbolic systems are not uniquely brittle, and explicitness can make their failures easier to diagnose.

The narrower claim is causal: formal assurance is purchased by restricting the admissible interpretations, and operational brittleness appears when the live world violates or escapes those restrictions. Latent models also compress the world, but their commitments are distributed across data and parameters. Logic concentrates them in vocabulary, axioms and inference semantics. That concentration creates both auditability and a crisp failure edge.

Defeater. The thesis would be weakened by a system that could expand and revise its ontology across genuinely novel categories, preserve formally stated guarantees, maintain grounding and closure evidence, and do so without human remodelling or a hidden shift to probabilistic judgement. Current formalisms solve bounded pieces of that problem, not the whole combination.

Negative control: try the simpler mechanism first

Suppose the waiver task has one product table, one verified-evidence table and one restriction table, all complete and synchronised. The eligibility rule is short, changes rarely and is owned by one application. A typed function plus database constraints may provide the same determinism, traceability and testability with less machinery. An ontology reasoner would add little.

This is the necessary negative control. Without it, teams can attribute benefits of ordinary software discipline to “knowledge representation”. A relational schema already makes entities, keys and cardinalities explicit. SQL constraints can reject malformed state. A decision table can express a small policy. A conventional test suite can verify expected behaviour across the cases it covers.

Symbolic KR earns its cost when the problem needs one or more additional properties: shared semantics across systems; class and relation inference; many interacting rules; consistency checking; countermodel construction; query over partially known data; explicit default or temporal reasoning; or portable explanations tied to a formal vocabulary. If the simpler baseline preserves the required distinctions and evidence, use it.

Choose the lightest mechanism that preserves the needed commitment A decision map places validation, typed code, ontology and rules, probabilistic models and human judgement according to semantic stability and whether the task needs derivation rather than checking. Representation choice map semantic stability and closure → need for derived consequences → validation schema · SHACL · constraints typed code small, closed decision ontology + rules shared semantics · derivation probabilistic model fuzzy or incomplete signals human judgement contested meaning or authority Semantic stability does not imply low consequence. Consequence determines controls around the mechanism.
Figure 8. Use the lightest mechanism that preserves the required distinctions. Practitioner decision instrument. Placement is qualitative and illustrative; it is not a benchmark result.
Part IV

Engineering a bounded symbolic layer

The practical objective is not to encode the enterprise or the world. It is to create a representation whose commitments are narrow enough to defend and rich enough to change a decision. Begin with a consequential query, then model only the distinctions required to answer it and reject unsafe cases.

The commitment audit

For every predicate used in a consequential rule, maintain a small typed record. The record makes visible the assumptions that prose and diagrams usually hide. The example below applies to the synthetic restriction predicate.

Predicate
active_hold(account, as_of)
Meaning
An enforceable restriction recorded against the account at the stated observation time.
Grounding source
Authoritative restriction snapshot keyed by stable account identifier.
Typing
First argument is an account; second is an observation time.
Closure
Closed only when the snapshot is complete for the account population and freshness window.
Unknown handling
Block the waiver rule and request readback; do not convert absence to false.
Defeaters
Feed health failure, identifier merge, stale watermark, unresolved duplicate.
Tests
Positive hold, absent hold under closure, absent hold without closure, stale snapshot.

This card is design inference, not a standard. Its purpose is to bind five questions to one predicate: what it denotes, how it is typed, what source grounds it, when absence is meaningful, and what can defeat its use. The rule engine then consumes the card’s machine-readable fields rather than relying on tribal knowledge.

Build from the query backwards

Start with the conclusion the system must support. Define whether it is an observation, a derived claim, a recommendation or an authorised decision. List the minimum premises. For each premise, decide whether it comes from a source record, a deterministic calculation, a human judgement or another inference. This prevents a generated label from silently becoming a fact.

Next, state the domain and time. owns(c,a) may be enough for a static teaching example. A live system may need owns(c,a,t), a validity interval, or an event-sourced relation. Time is not a metadata garnish when it changes whether the rule is true.

Then specify closure per predicate. Some relations may be complete within a snapshot, while others remain open. RDF semantics is monotonic: adding information does not cancel earlier entailments.[7] Closed-world and default conclusions are context-bound. If the system makes their context explicit, it can keep the resulting claim scoped rather than letting it travel as timeless truth.

Separate inference from validation and authority

Validation asks whether an input meets structural and value constraints. Inference asks what follows from accepted statements. Authority asks who may approve or execute an effect. A graph, ontology or rule engine does not answer the third question merely because it can express the first two.

In the running case, the rule derives waiver_candidate. It should not execute a fee change. The consuming workflow still needs identity, policy, current world state, action limits and outcome verification. This is not a weakness of logic. It is a system boundary that should remain visible.

Test the representation, not only the engine

  1. Reference tests. Verify that identifiers and source events map to the intended entities and states, including merges, duplicates and stale records.
  2. Entailment tests. Provide minimal fact sets that should derive each conclusion and countermodels that should prevent it.
  3. Unknown tests. Remove each premise in turn. Confirm that missing information remains unknown unless a documented closure contract applies.
  4. Exception tests. Add specific defeaters, conflicting defaults and expired exceptions. Check priority and retraction behaviour explicitly.
  5. Mutation tests. Change class relationships, rule operators and time boundaries. A useful suite should fail when a meaningful commitment changes.
  6. Baseline tests. Compare the ontology and reasoner with typed code, a decision table or constraints. Keep the symbolic layer only if it earns its additional cost.

These tests make representation quality falsifiable. They also reveal a common anti-pattern: testing only examples that the ontology was built to encode. A serious evaluation includes category boundary cases, missing facts, stale sources and plausible alternative interpretations.

Use probabilistic components without converting uncertainty into fact

A classifier may be the best way to detect a document type, map a phrase to a concept or estimate whether evidence is relevant. A symbolic layer can then enforce stable consequences. The interface must preserve uncertainty. A model proposal such as “0.72 probability of support need” should not arrive as the unqualified fact verified_need(asha).

Possible treatments include a human confirmation, a deterministic threshold with calibration evidence, a separate predicate such as candidate_need, or an inference formalism that represents uncertainty directly. The choice depends on consequence and evidence. The durable rule is that a change of representation type must not erase epistemic status.

Architecture decision. Adopt a symbolic layer only when the team can name the intended query, ground its predicates, defend closure and exception semantics, test countermodels, and show that a simpler constraint or typed-code baseline loses a required capability.

This paper is adjacent to Knowledge Architecture as a Design Discipline, which addresses corpus authority, metadata, lifecycle and retrieval. The present question is narrower: once a machine has candidate facts, what explicit commitments let it derive a conclusion, and where do those commitments fail?

Compact glossary

Symbol
A manipulable token used to denote an entity, class, relation or other object of discourse.
Predicate
A property or relation that becomes true or false under an interpretation.
Ontology
An explicit specification of the classes, relations and commitments used to describe a domain.
Axiom
A statement accepted by the theory rather than derived within it.
Interpretation
An assignment of denotations and relations that determines whether sentences are true.
Entailment
A relation in which a conclusion is true in every interpretation satisfying the premises.
Monotonic
Adding premises cannot invalidate an earlier entailment.
Closed world
A scoped assumption that unrecorded positive facts are false because the relevant record is complete.
Defeasible
Capable of being withdrawn when a defeating fact or stronger rule appears.
Grounding
The connection by which a symbol is tied to the entity, observation or state it is intended to denote.

Make the boundary part of the representation

Knowledge representation does something unusually valuable: it lets a system expose the terms in which it sees a domain and the steps by which a conclusion follows. Symbols name. Predicates state. Ontologies organise commitments. Rules license consequences. Model-theoretic semantics says exactly what a proof guarantees.

That guarantee is conditional. It begins after symbols have been grounded, after categories have been chosen, after the treatment of absence has been fixed, and after exceptions have been bounded. The proof can be impeccable while the world has already moved outside the model.

The changed engineering decision is to treat closure, grounding, context and defeaters as first-class parts of every consequential predicate. Do not ask whether logic is better than learning in the abstract. Ask which distinctions are stable enough to formalise, which observations are complete enough to negate, which conclusions need a trace, and which uncertainties must remain outside the rule engine.

Used this way, logic is neither a universal theory of intelligence nor a nostalgic alternative to statistical models. It is a disciplined instrument for bounded worlds. Its brittleness is not a reason to hide the boundary. It is the reason to make the boundary executable.

Sources

Open the source register and extended notes
  1. Randall Davis, Howard Shrobe and Peter Szolovits, “What Is a Knowledge Representation?”, AI Magazine 14(1), 1993. Primary conceptual source.
  2. John McCarthy and Patrick J. Hayes, “Some Philosophical Problems from the Standpoint of Artificial Intelligence”, Machine Intelligence 4, 1969; indexed on McCarthy’s Stanford archive. Primary source for situation calculus and logical AI.
  3. Raymond Reiter, “A Logic for Default Reasoning”, Artificial Intelligence 13, 1980. Primary source for default logic.
  4. Stevan Harnad, “The Symbol Grounding Problem”, Physica D 42, 1990. Primary source; the hosted text records the original publication.
  5. Thomas R. Gruber, “A Translation Approach to Portable Ontology Specifications”, Knowledge Acquisition 5(2), 1993. Primary ontology source.
  6. W3C, RDF 1.1 Concepts and Abstract Syntax, Recommendation. Official data-model specification.
  7. W3C, RDF 1.1 Semantics, Recommendation. Official model-theoretic semantics.
  8. W3C, OWL 2 Web Ontology Language Primer, Second Edition, Recommendation. Official explanation of OWL entities, entailment and open-world semantics.
  9. W3C, OWL 2 Web Ontology Language Profiles, Second Edition, Recommendation. Official expressiveness and reasoning-efficiency profiles.
  10. W3C, Shapes Constraint Language (SHACL), Recommendation. Official RDF validation specification.
  11. Charles L. Forgy, “Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem”, Artificial Intelligence 19(1), 1982. Primary implementation source.
  12. Ernest Davis, “Logical Formalizations of Commonsense Reasoning: A Survey”, Journal of Artificial Intelligence Research 59, 2017. Authoritative research survey and limitation source.
  13. Federica Di Stefano, Quentin Manière, Magdalena Ortiz and Mantas Šimkus, “Minimal Model Reasoning in Description Logics: Don’t Try This at Home!”, arXiv:2508.05350, 2025. Recent primary theoretical preprint; used only for its stated complexity results.
  14. Rajesh Ranjan Mahapatra, “Knowledge Architecture as a Design Discipline”. Adjacent practitioner article on corpus authority, lifecycle and retrieval.