Architecture Part 6

Proof Traces

Deterministic explanation of how an answer was derived.

Concept

In CNL-PL, an answer (Boolean, Set, or Plan) is rarely enough. Users need to know why. The ProofTrace object is a standard contract returned by almost all pragmatic engines.

Trace Structure (DS18)

{
  kind: "ProofTrace",
  mode: "Derivation" | "Witness" | "PlanSearch" | "SolveSearch" | ...,
  conclusion: "Socrates is mortal",
  answerSummary: "True",
  steps: [
    "Applied rule: Every man is mortal.",
    "Therefore: Socrates is mortal."
  ],
  premises: [
    "Socrates is a man."
  ]
}

Modes

Derivation

Used for atomic facts. Shows the rule chain and base premises (axioms) used to derive the fact.

Witness

Used for Queries. For every entity returned (e.g., "John"), it provides the specific facts that satisfied the query filters.

PlanSearch

Used for Planning. Lists the chosen action sequence and validates preconditions for each step.

SolveSearch

Used for CSP. Shows key search decisions (branching) and backtracks, proving the solution is consistent.

Reference

Defined in DS18 - Proof Traces.