Computational Knowledge and Reasoning

For 2,500 years, epistemology—the philosophical study of knowledge—has asked: What distinguishes genuine knowledge from mere opinion? The classical answer, traceable to Plato's Theaetetus, holds that knowledge requires three conditions: Belief (you must hold the proposition), Truth (the proposition must be true), and Justification (you must have good reasons for believing it).

This analysis—knowledge as Justified True Belief (JTB)—has been refined, challenged (notably by Gettier in 1963), and extended over millennia. But for computational systems, we must ask a more practical question: What can we actually implement?

Truth, in the philosophical sense, is correspondence with reality. A proposition is true if the world is actually the way the proposition says it is. But this correspondence relation is external to any representation. No system can verify truth by inspecting its own data structures—truth requires comparing representations to reality itself.

What systems can verify is logical truth (truth-preserving inference from premises) and coherence (consistency with other beliefs). But material truth—correspondence with the external world—remains beyond verification. We must make peace with this limitation.

Justification—having good reasons for belief—is precisely what computational systems can implement. And in computational terms, justification takes three forms:

• Provenance answers: What source document, sensor reading, or testimony grounds this claim? At what location in that source? With what extraction confidence?
• Proof answers: What premises were used? What inference rules were applied? Can the derivation be independently verified?
• Context answers: When does this hold (temporal scope)? For which entities (entity resolution)? Under what domain constraints? Within what ontological frame?

Together, provenance, proof, and context constitute computational justification. A system that provides all three for its claims is a system whose claims are justified—which is what epistemology always required.

• Provenance implements foundationalism—the view that justification terminates in basic beliefs grounded in perception or testimony.
• Proof implements inferentialism—the view that beliefs can be justified by derivation from other beliefs via valid inference.
• Context implements situatedness—the view that knowledge is always indexed to time, domain, and ontological frame.
• Defeaters (rebutting and undercutting evidence) map to UNSAT cores and counterexamples.
• The Gettier problem (justified true belief that isn't knowledge due to luck) becomes a provenance quality problem—tracing whether sources themselves had knowledge.

The AI industry processes data—tokens in, tokens out, no understanding. That's why LLMs hallucinate: they're coherentist systems that match patterns without justification. Knowledge requires something data doesn't have: provenance, proof, and context. We are entering an era where unjustified claims are produced at unprecedented scale:

• Large language models generate confident, fluent text with no grounding whatsoever
• Content farms produce SEO-optimized AI-generated material at industrial scale
• Hallucinations are linguistically indistinguishable from facts
• Synthetic content pollutes the information environment
• Users have no way to verify claims or trace their origins

The response to "how do you know this?" is increasingly just... nothing. A shrug. "The AI said so." This is the unjustified assertion that epistemology has warned against since Plato—now produced at machine scale.

1.4.1 Scarcity Creates Value

As unjustified claims become ubiquitous, justified claims become rare—and therefore valuable. It is the same economics that makes authenticated art worth more when counterfeits flood the market: provenance signals quality when fakes are everywhere.

A system known for justified claims builds reputation over time. Wikipedia won against Encarta not by being more authoritative but by being more transparent about sources. "Citation needed" became the rallying cry. Proof, provenance, and context operationalizes "citation needed" for the AI era.

1.4.2 Two Markets Emerging

Not all use cases require justification. But two distinct markets are emerging:

The slop market is large but commoditized. The justified market is smaller but defensible and high-margin. More importantly: high-stakes domains cannot use slop. You cannot approve a drug, operate a power grid, make a legal argument, or commit capital based on "the AI said so." Enterprise and regulated environments require audit trails.

1.4.3 Legal Liability Is Coming

When AI-generated content causes harm—and it will, increasingly—the ability to demonstrate due diligence becomes legally essential. "We verified; here is the proof; here is the source; here is the context" is a defensible position. "The model generated it" is not. Systems without justification are liability exposure.

1.4.4 AI Verifying AI

As AI generates more content, AI must verify more content. But you cannot have another LLM "feel" whether something is true—that just moves the problem. The only way to verify at scale is formal methods: proofs that can be checked and provenance that can be traced. This is the role of the reasoning systems surveyed in this paper.

1.4.5 The Value Proposition

Proof, provenance, and context positions systems as the antidote to AI slop: Unlike systems that generate plausible-sounding answers, we provide proof (how was this derived?), provenance (where did this come from?), and context (under what conditions does this hold?) for every claim. In a world of AI slop, we offer justified knowledge. As noise increases, signal becomes more valuable. Proof, provenance, and context is how you demonstrate you are signal, not noise.

Not all knowledge is justified the same way. Following Russell and Ryle, we distinguish types of knowledge that require different justificatory structures.

2.1 Propositional Knowledge (Knowing-That)

Knowledge of facts: "The boiling point of water is 100°C." This is the primary domain of proof, provenance, and context:

• Grounded propositions: Justified by provenance → source document, location, extraction method
• Derived propositions: Justified by proof → premises, inference rules, verification
• Situated propositions: Qualified by context → temporal scope, domain constraints, entity resolution

2.2 Knowledge by Acquaintance (Knowing-What)

Direct experiential knowledge: "The taste of coffee." Justified by perceptual provenance—grounding in sensory data (images, audio, video) with region pointers. Propositions extracted from perceptual content inherit provenance from that content.

2.3 Procedural Knowledge (Knowing-How)

Skill knowledge: "How to ride a bicycle." May be represented as action sequences, plans, or policies. Justified by verification of goal achievement—proof that the procedure accomplishes its intended purpose under specified conditions (context).

We now formalize the representation of knowledge with its justificatory structure.

3.1 Schema Definition

A knowledge unit is represented as:

3.2 The Justification Structure (J)

J is the core of the schema—it contains the proof, provenance, and context that justify the claim:

J = {
  // PROVENANCE (for grounded knowledge)
  grounding: →G | null,          // Source pointer
  source_type: SourceType,       // perception | testimony | memory
  source_reliability: [0,1],     // Assessed reliability
  extraction_confidence: [0,1],  // Extraction quality

  // PROOF (for derived knowledge)
  inference_chain: InferenceChain | null, // Derivation

  // CONTEXT (for situated knowledge)
  kg_neighborhood: Set<κ>,       // Related knowledge units
  entity_resolution: EntityMap,  // Which entities this applies to
  domain_constraints: Set<constraint>, // Domain-specific rules
  ontology_frame: OntologyRef,   // Conceptual framework

  // DEFEATERS
  defeaters: Set<defeater>,      // Evidence against
  corroborators: Set<κ>,         // Supporting evidence
  confidence: [0,1]              // Overall justification strength
}

3.2.1 Provenance: The Grounding Pointer (→G)

For knowledge from sources (perception, testimony), provenance is captured by the grounding pointer:

→G = (source_id, modality, region)
• source_id: Unique identifier for the source document, image, recording, etc.
• modality: text | image | audio | video | sensor | ...
• region: Precise location—character span, bounding box, time interval, etc.

This answers: Where exactly did this claim come from? The claim is justified because we can point to its source.

3.2.2 Proof: The Inference Chain

For derived knowledge (from reasoning), proof is captured by the inference chain:

InferenceChain = {
  premises: List<κ>,                 // Input knowledge units
  inference_type: InferenceType,     // deductive | inductive | abductive | refutation | counterfactual
  rule: InferenceRule,               // The rule applied
  proof_object: ProofObject | null,  // Machine-checkable certificate
  verifier: VerificationSystem | null, // What verified this
  counterexample: Witness | null,    // For disproof
  assumptions: List<κ> | null,       // For counterfactuals
  reasoning_trace: List<step> | null // For neural reasoning (CoT)
}

This answers: How exactly was this claim established? The claim is justified because we can trace its derivation from premises through verified inference.

3.2.3 Context: The Situating Frame

Knowledge is never context-free. A claim that holds in one context may not hold in another. Context is captured by:

• Temporal scope (τ): When does this hold? Past, present, future? What time interval?
• KG neighborhood: What related knowledge units situate this claim?
• Entity resolution: Which specific entities does this apply to?
• Domain constraints: What domain-specific rules govern this claim?
• Ontology frame: What conceptual framework organizes the entities and relationships?

3.3 Epistemic Modality (μ)

The modal value indicates the epistemic status of the claim:

In 1963, Edmund Gettier showed that justified true belief is not sufficient for knowledge. Gettier cases arise when justification and truth are disconnected by luck. These cases are directly relevant to computational systems.

4.1 The Computational Gettier Case

A RAG system retrieves a document stating "Company X revenue is $4.2M." The system has a claim (the assertion), provenance (the document, location, extraction), and truth (the revenue actually is $4.2M). But the document's author guessed—they had no data. The guess was coincidentally correct. Does the system know the revenue? Intuitively, no. The provenance is intact, but the source itself lacked knowledge. Provenance alone doesn't guarantee knowledge—it matters whether the source had proper epistemic standing.

4.2 Provenance Quality and Context

The solution involves both provenance quality and context:

1. Did the source know? (Not merely believe truly)
2. Was the source sincere? (Not intending to deceive)
3. Was the source competent? (In the relevant domain)
4. Are there undefeated defeaters? (Evidence against the source)
5. Is the context appropriate? (Does the source's context match the query's context?)

If proof is one pillar of justification, then automated reasoning systems are proof generators. A mature ecosystem exists: theorem provers (Lean, Coq, Isabelle) produce machine-checkable proofs; SAT/SMT solvers (Z3, CVC5) determine satisfiability and generate counterexamples; logic programming engines (Datalog, Prolog) derive conclusions with traceable derivations; and causal reasoners implement Pearl's do-calculus for counterfactual inference.

These technologies have been deployed at enterprise scale—AWS invokes SMT-based policy verification millions of times daily. The feasibility of formal reasoning in production systems has been demonstrated.

While formal theorem provers represent the ideal for machine-checkable proof, practical systems must implement verification with available technologies. This section describes a multi-stage verification architecture that approximates proof through layered defense—each stage catching what previous stages missed.

6.1 The Problem: LLM Synthesis Without Verification

When an LLM synthesizes a response from retrieved sources, multiple error types can occur:

• Polarity inversion: "Low cognitive engagement supports reserve" when the source says the opposite
• Fabricated categories: Inventing labels like "service excellence" that don't appear in sources
• Numerical drift: "Less than 13 percent" when the source says a different number
• Ungrounded inference: Conclusions not supported by any source
• Structural non-compliance: Ignoring query instructions about format, filtering, or sorting

No single verification method catches all error types. The solution is layered defense.

6.2 Architecture: Four-Stage Verification Pipeline

6.3 Correction Strategies

Key principle: Corrections are themselves verified. A surgical rewrite triggers re-verification of the rewritten portion. If re-verification fails, escalate to full regeneration.

6.4 Design Principles

1. Layered defense: Each stage catches what previous stages missed. No single method is sufficient.
2. Cheap checks first: Lexical/structural checks before expensive LLM calls. Fail fast when possible.
3. No silent deletion: Flag and regenerate, never silently remove content. Omission is also an error.
4. Separation of concerns: Factual grounding, structural compliance, and style are distinct verification dimensions.
5. Verification of corrections: Every correction is re-verified. The cure must not be worse than the disease.

6.5 Relation to Formal Proof

This multi-stage pipeline is not formal proof—it provides probabilistic verification through redundant checks rather than mathematical certainty. But it demonstrates the architectural commitment to justification that formal methods would strengthen:

• Where the pipeline uses embedding similarity, formal methods would use entailment provers
• Where the pipeline uses LLM-based claim verification, formal methods would use SAT/SMT solvers
• Where the pipeline detects numerical drift heuristically, formal methods would verify arithmetic constraints
• Where the pipeline re-verifies corrections probabilistically, formal methods would provide machine-checkable proof of correction validity

7.1 Foundationalist Systems: Explicit Knowledge

Knowledge graphs, databases, and RAG systems are foundationalist: claims trace to sources (the foundations). Characterized by:

• Provenance: Every claim has a source pointer
• Inspectability: Justification can be examined
• Updateability: Sources can be corrected, claims updated
• Failure mode—omission: Cannot provide what is not in sources

7.2 Coherentist Systems: Parametric Knowledge

Large language models are coherentist: outputs are justified by coherence with training, not by source pointers. Characterized by:

• No provenance: Cannot point to where claims came from
• Holistic: Knowledge distributed across weights
• Generative: Can produce claims not in training
• Failure mode—commission: Produces plausible but false claims (hallucination)

7.3 Neither Addresses Context

Neither pure foundationalism nor pure coherentism adequately addresses context—the conditions under which knowledge holds. A claim may have perfect provenance but apply to the wrong time period. A derivation may be valid but use premises from an incompatible domain. Context is the third pillar that situates knowledge properly.

7.4 Neuro-Symbolic Integration: Complementary Strengths

Hybrid systems combine all three:

• Foundationalist layer: Provides provenance, grounds claims in sources
• Reasoning layer: Provides proof, extends knowledge through verified inference
• Contextual layer: The KG neighborhood that situates each claim—temporal scope, entity resolution, domain constraints
• Neural layer: Provides fluency, fills gaps, guides search
• Verification layer: Multi-stage pipeline combining symbolic and LLM-based verification with regeneration, resynthesis, surgical rewrites, and re-verification

Each layer compensates for others' weaknesses. The result: justified claims with proof, provenance, and context.

Classical epistemology identifies knowledge as Justified True Belief. But in computational systems:

• Truth cannot be verified (correspondence with reality is external)
• Belief is merely the assertion
• Justification is exactly what we can and must implement

This paper has argued that justification in computational systems takes three forms:

The knowledge unit schema κ = (S, P, O, τ, μ, J) provides a formal specification for representing claims with their justificatory structure. The J component records provenance (→G), proof (InferenceChain), and context (KG neighborhood, entity resolution, domain constraints, ontology frame).

Building such systems remains the challenge ahead. The theoretical framework developed here provides the conceptual foundation and formal specification. The candidate technologies surveyed demonstrate feasibility. What remains is implementation: integrating formal reasoning into knowledge system architectures to deliver justified knowledge at scale.

From Plato's analysis of knowledge to the pramāṇa tradition of India, from the Mohist Canons to Islamic logic—the thread across civilizations is continuous: justify your claims. Proof, provenance, and context are how computational systems can finally do so.