Design Philosophy

The symbolic engine prioritizes:

• Determinism: Same input always produces same output
• Traceability: Proof traces for every conclusion (audit logging/export is external)
• Correctness: No false positives from similarity thresholds
• Explainability: Every step can be explained and verified

Architecture Overview

Proof Strategy

The ProofEngine tries strategies in strict priority order. The first successful strategy returns the result:

Priority	Strategy	Description	Confidence
1	Direct KB Match	Exact vector match in knowledge base (strong threshold)	Very high (>0.95)
1.5	Synonym Match	Match via ComponentKB synonym expansion	High (0.95)
2	Transitive Chain	Follow isA/locatedIn/partOf chains to target	Decays with chain length
2.5	Property Inheritance	Inherit properties from parent classes	Based on chain confidence
3	Rule Matching	Backward chaining through rules (If/Then)	Product of condition confidences
4	Weak Direct Match	Accept lower-threshold KB matches	Moderate (>0.85)
5	Disjoint Proof	Prove via spatial/set negation	Variable

Core Classes

ProofEngine

Main orchestrator for proof search. Coordinates all reasoning components.

import { ProofEngine } from './reasoning/prove.mjs';

const engine = new ProofEngine(session, {
  maxDepth: 10,      // Maximum recursion depth
  timeout: 5000      // Timeout in milliseconds
});

// Prove a goal
const result = engine.prove({
  type: 'Statement',
  operator: { name: 'isA' },
  args: [{ name: 'Tweety' }, { name: 'Animal' }]
});

console.log(result);
// {
//   valid: true,
//   confidence: 0.9025,
//   method: 'transitive_chain',
//   steps: [
//     { operation: 'transitive_step', fact: 'isA Tweety Bird' },
//     { operation: 'transitive_step', fact: 'isA Bird Animal' }
//   ],
//   reasoningSteps: 4
// }

Key Methods

Method	Description
prove(goal)	Main entry point. Proves a goal statement and returns result with steps.
tryDirectMatch(vec, str)	Attempt direct KB match for goal vector.
combineConfidences(results)	Combine confidences from multiple sub-proofs with decay.
isGoalNegated(goal)	Check if goal is explicitly negated in KB.

QueryEngine

Handles queries with "holes" (unknown values to find). Uses the HDC Master Equation.

import { QueryEngine } from './reasoning/query.mjs';

const engine = new QueryEngine(session);

// Query: "What is Tweety?" (isA Tweety ?what)
const result = engine.execute({
  type: 'Statement',
  operator: { name: 'isA' },
  args: [
    { name: 'Tweety', type: 'Identifier' },
    { name: 'what', type: 'Hole' }
  ]
});

console.log(result);
// {
//   success: true,
//   bindings: Map { 'what' => { answer: 'Bird', similarity: 0.95, method: 'direct' } },
//   allResults: [
//     { bindings: Map {...}, score: 0.95, method: 'direct' },
//     { bindings: Map {...}, score: 0.90, method: 'transitive' }
//   ]
// }

Query Sources

QueryEngine aggregates results from multiple sources:

1. HDC Master Equation: Answer = KB BIND Query⁻¹
2. Direct KB Search: Exact metadata matching
3. Transitive Reasoning: Chain traversal for hierarchy queries
4. Rule Derivation: Apply rules to derive new bindings
5. Compound CSP: Multi-variable constraint solutions
6. Bundle Patterns: Common property discovery

Reasoning Sub-Components

TransitiveReasoner

Handles transitive relations with automatic chain discovery.

// Supported transitive relations
const TRANSITIVE_RELATIONS = new Set([
  'isA',          // Taxonomy chains
  'locatedIn',    // Spatial containment
  'partOf',       // Mereological relations
  'subClassOf',   // Class hierarchies
  'ancestorOf',   // Genealogy
  'contains',     // Inverse of locatedIn
  'before'        // Temporal ordering
]);

ConditionProver

Proves compound conditions with And/Or logic and backtracking.

// And condition: all must succeed
And(isA ?x Bird, can ?x Fly)

// Or condition: any can succeed
Or(isA ?x Penguin, isA ?x Ostrich)

PropertyInheritanceReasoner

Inherits properties from parent classes in the taxonomy.

// Given: Bird can Fly, Tweety isA Bird
// Proves: Tweety can Fly (via property inheritance)

CSP Solver

Constraint Satisfaction Problem solver for assignment problems.

import { CSPSolver } from './reasoning/csp/solver.mjs';

const solver = new CSPSolver(session);

// Wedding seating problem
solver.addVariable('Alice', ['Table1', 'Table2', 'Table3']);
solver.addVariable('Bob', ['Table1', 'Table2', 'Table3']);
solver.addVariable('Carol', ['Table1', 'Table2', 'Table3']);

// Constraints
solver.addNoConflict('Alice', 'Bob');  // Alice and Bob can't sit together
solver.addAllDifferent('Alice', 'Bob', 'Carol');  // All at different tables

const result = solver.solve();
// { success: true, solutions: [{ Alice: 'Table1', Bob: 'Table2', Carol: 'Table3' }, ...] }

Confidence Calculation

Confidence values decay through reasoning chains:

// Strategy-dependent thresholds (from constants.mjs)
const thresholds = {
  VERY_STRONG_MATCH: 0.95,   // Direct match threshold
  STRONG_MATCH: 0.85,        // Weak match threshold
  TRANSITIVE_BASE: 0.95,     // Base transitive confidence
  TRANSITIVE_DECAY: 0.95,    // Per-step decay factor
  DEFAULT_CONFIDENCE: 0.8    // When no explicit confidence
};

// Chain confidence: base * decay^length
// Example: 2-step chain → 0.95 * 0.95² = 0.857

Negation Handling

The engine checks for explicit negation before attempting proofs:

// If KB contains: Not $canTweetyFly (where $canTweetyFly = "can Tweety Fly")
// Then prove("can Tweety Fly") returns:
// { valid: false, reason: 'Goal is negated' }

Statistics Tracking

The engine tracks detailed reasoning statistics:

session.reasoningStats = {
  kbScans: 0,           // KB traversals
  similarityChecks: 0,  // HDC similarity computations
  ruleAttempts: 0,      // Rules tried
  transitiveChains: 0,  // Transitive inferences
  hdcQueries: 0,        // HDC Master Equation uses
  hdcSuccesses: 0,      // Successful HDC results
  // ...
};

Example: Complete Proof Trace

// KB: isA Tweety Bird, isA Bird Animal, can Bird Fly
// Query: prove "can Tweety Fly"

const result = engine.prove(parseGoal("can Tweety Fly"));

// Result:
{
  valid: true,
  confidence: 0.902,
  method: 'property_inheritance',
  goal: 'can Tweety Fly',
  steps: [
    {
      operation: 'find_class_property',
      fact: 'can Bird Fly',
      confidence: 0.95
    },
    {
      operation: 'verify_membership',
      fact: 'isA Tweety Bird',
      confidence: 0.95
    },
    {
      operation: 'inherit_property',
      from: 'Bird',
      to: 'Tweety',
      property: 'can Fly'
    }
  ],
  reasoningSteps: 6,
  proof: [...steps]
}

Integration with HDC

While symbolic reasoning drives decisions, HDC provides acceleration:

Limitations

• No fuzzy matching: Requires exact or near-exact matches
• Depth limits: Deep recursion may timeout
• Rule explosion: Many rules can slow backward chaining
• Closed-world assumption: Unprovable = false