Running Inference

The inference engine operates on rules and facts. Inference endpoints use psi() for term construction and plain JS values for features.

Adding rules

A rule has a head (conclusion) and antecedents (body/conditions). When all antecedents are satisfied, the head can be derived.

import {
  ReasoningLayerClient,
  psi,
} from '@kortexya/reasoninglayer';

const client = new ReasoningLayerClient({
  baseUrl: 'https://platform.ovh.reasoninglayer.ai',
  tenantId: 'my-tenant-uuid',
  auth: { mode: 'cookie' },
});

// Rule: grandparent(X, Z) :- parent(X, Y), parent(Y, Z)
const rule = await client.inference.addRule({
  term: psi('grandparent', {
    person: '?X',
    grandchild: '?Z',
  }),
  antecedents: [
    psi('parent', {
      person: '?X',
      child: '?Y',
    }),
    psi('parent', {
      person: '?Y',
      child: '?Z',
    }),
  ],
  certainty: 1.0,
});

console.log(rule.term.termId); // UUID of the created rule

Adding facts

Facts are ground terms (no variables) that serve as the knowledge base.

// Add individual facts
await client.inference.addFact({
  term: psi('parent', {
    person: 'Alice',
    child: 'Bob',
  }),
});

await client.inference.addFact({
  term: psi('parent', {
    person: 'Bob',
    child: 'Charlie',
  }),
});

Bulk operations

// Bulk-add facts
const factsResult = await client.inference.bulkAddFacts({
  facts: [
    psi('parent', {
      person: 'Alice',
      child: 'Bob',
    }),
    psi('parent', {
      person: 'Bob',
      child: 'Charlie',
    }),
  ],
});
console.log(factsResult.factsAdded); // 2

// Bulk-add rules — recursive definition of `ancestor`
// ancestor(X, Y) :- parent(X, Y).                       -- base case
// ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).       -- recursive step
const rulesResult = await client.inference.bulkAddRules({
  rules: [
    {
      term: psi('ancestor', {
        person: '?X',
        descendant: '?Y',
      }),
      antecedents: [
        psi('parent', {
          person: '?X',
          child: '?Y',
        }),
      ],
    },
    {
      term: psi('ancestor', {
        person: '?X',
        descendant: '?Y',
      }),
      antecedents: [
        psi('parent', {
          person: '?X',
          child: '?Z',
        }),
        psi('ancestor', {
          person: '?Z',
          descendant: '?Y',
        }),
      ],
    },
  ],
});
console.log(rulesResult.rulesAdded); // 2

See Recursive Rules for the base-case / recursive-step pattern, tabling, fixpoint semantics, and how to bound recursion safely.

Backward chaining

Backward chaining searches for matching data by working backwards through rules from your goal.

Using an inline goal

const result = await client.inference.backwardChain({
  goal: psi('grandparent', {
    person: '?Who',
    grandchild: 'Charlie',
  }),
  maxSolutions: 10,
  maxDepth: 50,
});

for (const solution of result.solutions) {
  console.log(`Certainty: ${solution.certainty}`);
  for (const binding of solution.substitution.bindings) {
    console.log(`  ${binding.variableName} = ${binding.boundToDisplay}`);
  }
}

console.log(`Query time: ${result.queryTimeMs}ms`);

Using a saved goal ID

You can save a goal for reuse and reference it by ID.

// Create and save a goal
const goalResult = await client.inference.createGoal({
  clauses: [
    psi('grandparent', {
      person: '?Who',
      grandchild: 'Charlie',
    }),
  ],
});

// Use the saved goal
const result = await client.inference.backwardChain({
  goalId: goalResult.goalId,
  maxSolutions: 5,
});

Dual input mode

Provide either goal (inline) or goalId (saved reference), never both.

Open-world reasoning

By default, backward chaining uses closed-world semantics. Enable openWorld for evidence-based reasoning that tolerates missing information.

const result = await client.inference.backwardChain({
  goal: psi('diagnosis', {
    condition: '?Condition',
  }),
  openWorld: true,
  minCertainty: 0.3,
});

for (const solution of result.solutions) {
  // Open-world solutions include evidence metrics
  console.log(`Evidence ratio: ${solution.evidenceRatio}`);
  console.log(`Matched: ${solution.evidenceMatched}`);
  console.log(`Residuated sorts: ${solution.residuatedSorts}`);
}

Timeouts

The timeoutMs field sets a wall-clock timeout for proof search. When it fires, the engine returns whatever solutions have been found so far.

const result = await client.inference.backwardChain({
  goal: psi('complex_query', {
    result: '?R',
  }),
  timeoutMs: 5000, // 5 second timeout
});
// result.solutions contains partial results if timeout occurred

Forward chaining

Forward chaining is data-driven materialization. It applies rules to existing facts to derive new facts.

const result = await client.inference.forwardChain({
  maxIterations: 100,
  maxFacts: 1000,
  persistDerived: true,
  enableProvenanceTags: true,
});

console.log(`Derived ${result.derivedCount} new facts`);
console.log(`Total facts: ${result.totalFacts}`);
console.log(`Iterations: ${result.iterations}`);
console.log(`Time: ${result.materializationTimeMs}ms`);

// Examine derived facts
for (const fact of result.derivedFacts) {
  console.log(`${fact.sortName}: ${fact.display}`);
}

// Provenance tags (when enabled)
if (result.provenanceTags) {
  for (const tag of result.provenanceTags) {
    console.log(`Fact[${tag.factIndex}] confidence: ${tag.confidence}`);
  }
}

Seeding with initial facts

const result = await client.inference.forwardChain({
  initialFacts: [
    psi('temperature', {
      location: 'server-room',
      value: 45,
    }),
  ],
  persistDerived: false,
});

Interpreting solutions

A SolutionDto contains variable bindings, an optional proof tree, and certainty information.

const result = await client.inference.backwardChain({
  goal: psi('ancestor', {
    person: '?Ancestor',
    descendant: 'Charlie',
  }),
});

for (const solution of result.solutions) {
  // Variable bindings
  for (const binding of solution.substitution.bindings) {
    console.log(`${binding.variableName} -> ${binding.boundToDisplay}`);
    // binding.variableTermId  -- UUID of the variable term
    // binding.boundToTermId  -- UUID of the bound value term
  }

  // Proof tree (if available)
  if (solution.proof) {
    printProof(solution.proof, 0);
  }

  // Certainty
  console.log(`Certainty: ${solution.certainty}`);
}

function printProof(proof, depth) {
  const indent = '  '.repeat(depth);
  console.log(`${indent}Goal: ${proof.goalTermId} (certainty: ${proof.certainty})`);
  if (proof.ruleTermId) {
    console.log(`${indent}  via rule: ${proof.ruleTermId}`);
  }
  for (const sub of proof.subproofs ?? []) {
    printProof(sub, depth + 1);
  }
}

Managing facts and goals

// List all facts
const facts = await client.inference.getFacts();

// Clear all facts
const cleared = await client.inference.clearFacts();
console.log(`Cleared ${cleared.factsCleared} facts`);

// List saved goals
const goals = await client.inference.listGoals();

// Get a specific goal
const goal = await client.inference.getGoal(goalId);

// Delete a saved goal
const deleteResult = await client.inference.deleteGoal(goalId);

Meta-sorts

The inference engine uses built-in meta-sorts for constraint handling. You can inspect them:

const metaSorts = await client.inference.getMetaSorts();
// Record<string, string> mapping meta-sort names to UUIDs
console.log(metaSorts.guardConstraint);  // UUID of the guard meta-sort

Convenience alias

nafProve is also available as proveWithNegation for developers who prefer a more descriptive method name.