Proof Engine Core

Home · Reasoning · Symbolic · Holographic Backward chaining proof search with confidence tracking

The Proof Engine implements goal-directed backward chaining to establish whether a proposition can be derived from the knowledge base. It returns not just a boolean result, but a complete proof trace with confidence scores.

1. Theoretical Foundation

Goal: Given a goal G and knowledge base KB, determine if KB ⊢ G (KB entails G).

Approach: Backward chaining - start from the goal and work backward to known facts.

prove(G) = match(G, KB) ∨ ∃rule(P → G) : prove(P)

A goal is proven if it directly matches a KB fact, or if there exists a rule whose consequent matches G and whose premises can all be proven.

2. Proof Search Algorithm

Backward Chaining Proof Search Goal: prove(G) Direct KB Match? Yes SUCCESS No Find rules: P → G For each rule: prove(premise) Recurse FAILURE
Algorithm: prove(goal, kb, depth, visited)
  1. Base cases:
    • If depth > MAX_DEPTH → return FAIL (prevent infinite loops)
    • If goal ∈ visited → return FAIL (cycle detection)
  2. Direct match: Search KB for facts matching goal
    • If exact match found → return SUCCESS with confidence 1.0
    • If similar match (≥ threshold) → return SUCCESS with similarity score
  3. Transitive chains: For transitive relations (isA, partOf, locatedIn)
    • Search for chains: X rel Y, Y rel Z → X rel Z
    • Confidence decays: c_chain = c₁ × c₂ × α
  4. Rule matching: Find rules whose consequent unifies with goal
    • For each matching rule R: (P₁ ∧ P₂ ∧ ... ∧ Pₙ) → G
    • Recursively prove each premise Pᵢ
    • If all premises proven → SUCCESS
    • Confidence: c_rule = min(c_p₁, ..., c_pₙ) × rule_confidence
  5. Failure: If no method succeeds → return FAIL

3. Confidence Model

Every proof step produces a confidence score between 0 and 1:

Proof Method Confidence Formula Typical Range
Direct KB match similarity(goal, fact) 0.95 - 1.0
Transitive chain (n steps) ∏ᵢ cᵢ × α^(n-1) 0.7 - 0.95
Rule application min(c_premises) × c_rule 0.6 - 0.9
Weak/fuzzy match similarity × β 0.4 - 0.7
Confidence Decay Parameter (α): Controls how quickly confidence decays in chains.
α = 0.95 (default)

For a 3-step chain with all steps at 1.0 confidence: 1.0 × 1.0 × 1.0 × 0.95² = 0.9025

4. Proof Trace Structure

The engine returns a complete proof trace for debugging and explanation:

{
  success: true,
  goal: { operator: 'isA', args: ['Socrates', 'Mortal'] },
  method: 'rule_application',
  confidence: 0.95,
  rule: '@r1: Implies (isA ?x Human) (isA ?x Mortal)',
  bindings: { '?x': 'Socrates' },
  premises: [
    {
      success: true,
      goal: { operator: 'isA', args: ['Socrates', 'Human'] },
      method: 'direct_kb',
      confidence: 1.0,
      matchedFact: 'isA Socrates Human'
    }
  ],
  depth: 1,
  steps: 2
}

5. Unification

Unification finds substitutions that make two expressions identical:

unify(isA ?x Human, isA Socrates Human) = { ?x → Socrates }

Variables (prefixed with ?) can match any term. Constants must match exactly.

Expression 1 Expression 2 Unification Result
loves ?x Mary loves John Mary { ?x → John }
isA ?x ?y isA Cat Animal { ?x → Cat, ?y → Animal }
isA Dog ?x isA Cat Animal FAIL (Dog ≠ Cat)

6. Compound Goals

The proof engine handles compound logical structures:

And: All subgoals must be proven 
prove(And(P, Q)) = prove(P) ∧ prove(Q)
confidence = min(c_P, c_Q)
Or: At least one subgoal must be proven 
prove(Or(P, Q)) = prove(P) ∨ prove(Q)
confidence = max(c_P, c_Q)
Not: Negation-as-failure (Closed World Assumption) 
prove(Not(P)) = ¬prove(P)
confidence = 1.0 - c_P (if P provable)
confidence = 1.0 (if P not provable)

7. Optimization Strategies

Strategy Description Impact
Memoization Cache proven/failed goals Avoids redundant proof attempts
Depth limiting Max recursion depth (default: 20) Prevents infinite loops
Cycle detection Track visited goals in current path Detects circular proofs
Rule ordering Try more specific rules first Finds proofs faster
HDC pre-filtering Use similarity to find candidates Reduces search space

8. Example: Syllogism Proof

Knowledge Base: 
isA Socrates Human
@r1 Implies (isA ?x Human) (isA ?x Mortal)
Goal: prove(isA Socrates Mortal) Proof Trace:
  1. Goal: isA Socrates Mortal
  2. Direct KB search → No match
  3. Find rules with consequent matching goal:
    • Rule @r1: Implies (isA ?x Human) (isA ?x Mortal)
    • Unify: { ?x → Socrates }
  4. Prove premise: isA Socrates Human
    • Direct KB match → SUCCESS (confidence: 1.0)
  5. All premises proven → Apply rule
  6. Result: SUCCESS (confidence: 0.95)

9. API Reference

import { ProofEngine } from 'agisystem2/reasoning';

const engine = new ProofEngine(session);

// Prove a goal
const result = await engine.prove({
  operator: 'isA',
  args: ['Socrates', 'Mortal']
});

// With options
const result = await engine.prove(goal, {
  maxDepth: 10,           // Limit recursion
  minConfidence: 0.5,     // Reject weak proofs
  includeTrace: true,     // Full proof trace
  timeout: 5000           // Max time (ms)
});

10. Related Documentation

← Back to Reasoning Engines