@cogitator-ai/neuro-symbolic

Neuro-symbolic AI package for hybrid neural-symbolic reasoning. Combines LLM-based understanding with formal methods for verifiable, explainable AI.

Installation

pnpm add @cogitator-ai/neuro-symbolic

For Z3 constraint solving support:

pnpm add z3-solver

Features

• Logic Programming - Prolog-style rules with unification and SLD resolution
• Knowledge Graph Queries - SPARQL-like query language with natural language interface
• Constraint Solving - SAT/SMT solving with Z3 WASM or pure-TS fallback
• Plan Verification - PDDL-like action schemas with invariant checking and repair

Quick Start

import {
  createNeuroSymbolic,
  ConstraintBuilder,
  variable,
  constant,
} from '@cogitator-ai/neuro-symbolic';

const ns = createNeuroSymbolic();

// Logic Programming
ns.loadLogicProgram(`
  parent(tom, mary).
  parent(mary, ann).
  grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
`);

const result = ns.queryLogic('grandparent(tom, X)?');
console.log(result.solutions); // X = ann

// Constraint Solving
const problem = ConstraintBuilder.create()
  .int('x', 1, 10)
  .int('y', 1, 10)
  .assert(variable('x').add(variable('y')).eq(constant(15)))
  .build();

const solution = await ns.solve(problem);
console.log(solution); // { x: 5, y: 10 } or similar

Logic Programming

Prolog-style logic programming with backward chaining and unification.

Loading Programs

import { createNeuroSymbolic } from '@cogitator-ai/neuro-symbolic';

const ns = createNeuroSymbolic();

// Load facts and rules
ns.loadLogicProgram(`
  % Facts
  human(socrates).
  human(plato).

  % Rules
  mortal(X) :- human(X).

  % Lists
  append([], L, L).
  append([H|T], L, [H|R]) :- append(T, L, R).
`);

Querying

// Simple query
const result = ns.queryLogic('mortal(socrates)?');
console.log(result.success); // true

// Query with variables
const result = ns.queryLogic('mortal(X)?');
for (const solution of result.solutions) {
  console.log(solution.get('X')); // socrates, plato
}

// Multiple solutions
const result = ns.queryLogic('append(X, Y, [1,2,3])?');
// X=[], Y=[1,2,3]
// X=[1], Y=[2,3]
// X=[1,2], Y=[3]
// X=[1,2,3], Y=[]

Proof Trees

import { formatProofTree, proofTreeToMermaid } from '@cogitator-ai/neuro-symbolic';

const result = ns.queryLogic('grandparent(tom, X)?');
console.log(formatProofTree(result.proofTree));
console.log(proofTreeToMermaid(result.proofTree)); // Mermaid diagram

Built-in Predicates

| Predicate | Description | | ---------------------------- | --------------------- | | is/2 | Arithmetic evaluation | | =/2 | Unification | | \+/1 | Negation as failure | | >/2, </2, >=/2, =</2 | Comparisons | | member/2 | List membership | | append/3 | List concatenation | | length/2 | List length | | reverse/2 | List reversal | | findall/3 | Collect all solutions | | !/0 | Cut |

Knowledge Graph Queries

SPARQL-like query language with natural language interface.

Query Builder

import { GraphQueryBuilder, variable, executeQuery } from '@cogitator-ai/neuro-symbolic';

const query = new GraphQueryBuilder()
  .select()
  .pattern(variable('person'), 'worksAt', 'Google')
  .pattern(variable('person'), 'hasSkill', variable('skill'))
  .filter('skill', 'contains', 'Python')
  .orderBy('person', 'asc')
  .limit(10)
  .build();

const result = await executeQuery(query, { adapter: graphAdapter, agentId: 'agent-1' });

Natural Language Queries

const result = await ns.askGraph('Who works at Google and knows Python?');
console.log(result.naturalLanguageResponse);

Reasoning Engine

import { createReasoningEngine, findPath, multiHopQuery } from '@cogitator-ai/neuro-symbolic';

const engine = createReasoningEngine(graphAdapter);

// Find path between entities
const path = await findPath(graphAdapter, 'Alice', 'CompanyX', { maxHops: 3 });

// Multi-hop query
const results = await multiHopQuery(graphAdapter, 'Alice', ['worksAt', 'locatedIn'], {
  maxHops: 2,
});

// Inference
const inferred = await engine.infer({
  enableTransitivity: true,
  enableInverse: true,
  enableComposition: true,
});

Constraint Solving

SAT/SMT solving with fluent DSL.

Building Constraints

import {
  ConstraintBuilder,
  variable,
  constant,
  and,
  or,
  not,
  allDifferent,
} from '@cogitator-ai/neuro-symbolic';

const problem = ConstraintBuilder.create()
  // Define variables
  .bool('a')
  .bool('b')
  .int('x', 0, 100)
  .int('y', 0, 100)
  .real('z', 0.0, 1.0)

  // Add constraints
  .assert(variable('a').or(variable('b')))
  .assert(variable('x').add(variable('y')).lte(constant(50)))
  .assert(variable('z').mul(constant(2)).gt(constant(0.5)))
  .assert(allDifferent(variable('x'), variable('y')))

  // Optimization objective
  .maximize(variable('x').add(variable('y')))

  .build();

const result = await solve(problem);
if (result.status === 'sat') {
  console.log(result.model.assignments);
}

Solver Selection

import { isZ3Available, createZ3Solver, createSimpleSATSolver } from '@cogitator-ai/neuro-symbolic';

// Check Z3 availability
if (await isZ3Available()) {
  const solver = await createZ3Solver();
  const result = await solver.solve(problem);
} else {
  // Fallback to pure-TS solver
  const solver = createSimpleSATSolver();
  const result = solver.solve(problem);
}

Expression Types

// Arithmetic
variable('x').add(variable('y'));
variable('x').sub(constant(5));
variable('x').mul(constant(2));
variable('x').div(constant(3));

// Boolean
variable('a').and(variable('b'));
variable('a').or(variable('b'));
not(variable('a'));
variable('a').implies(variable('b'));
variable('a').iff(variable('b'));

// Comparisons
variable('x').eq(constant(10));
variable('x').neq(variable('y'));
variable('x').gt(constant(0));
variable('x').gte(constant(0));
variable('x').lt(constant(100));
variable('x').lte(constant(100));

// Global constraints
allDifferent(variable('x'), variable('y'), variable('z'));
atMost(2, variable('a'), variable('b'), variable('c'));
atLeast(1, variable('a'), variable('b'), variable('c'));
exactly(1, variable('a'), variable('b'), variable('c'));

Plan Verification

PDDL-like planning with verification and repair.

Action Schemas

import { ActionSchemaBuilder, ActionRegistry } from '@cogitator-ai/neuro-symbolic';

const moveAction = new ActionSchemaBuilder('move')
  .description('Move robot from one location to another')
  .parameter('from', 'string', true)
  .parameter('to', 'string', true)
  .precondition({ type: 'simple', variable: 'robotAt', value: '${from}' })
  .precondition({ type: 'comparison', variable: 'battery', operator: 'gt', value: 10 })
  .effect({ type: 'assign', variable: 'robotAt', value: '${to}' })
  .effect({ type: 'decrement', variable: 'battery', amount: 5 })
  .cost(5)
  .build();

const registry = new ActionRegistry();
registry.register(moveAction);

Plan Validation

import { validatePlan, formatValidationResult } from '@cogitator-ai/neuro-symbolic';

const plan = {
  id: 'plan-1',
  actions: [
    { id: 'a1', schemaName: 'move', parameters: { from: 'A', to: 'B' } },
    { id: 'a2', schemaName: 'move', parameters: { from: 'B', to: 'C' } },
  ],
  initialState: { id: 's0', variables: { robotAt: 'A', battery: 100 } },
  goalConditions: [{ type: 'simple', variable: 'robotAt', value: 'C' }],
};

const result = validatePlan(registry, plan);
console.log(formatValidationResult(result));

Invariant Checking

import { createInvariantChecker, formatInvariantResults } from '@cogitator-ai/neuro-symbolic';

const checker = createInvariantChecker(registry);

// Add safety properties
checker.addInvariant('battery-non-negative', {
  type: 'comparison',
  variable: 'battery',
  operator: 'gte',
  value: 0,
});

checker.addNever('collision', {
  type: 'and',
  conditions: [
    { type: 'simple', variable: 'robotAt', value: 'danger-zone' },
    { type: 'simple', variable: 'alarmActive', value: false },
  ],
});

checker.addEventually('goal-reached', {
  type: 'simple',
  variable: 'goalAchieved',
  value: true,
});

const results = checker.checkPlan(plan);
console.log(formatInvariantResults(results));

Plan Repair

import { createPlanRepairer, formatRepairResult } from '@cogitator-ai/neuro-symbolic';

const repairer = createPlanRepairer(registry, {
  maxInsertions: 3,
  maxRemovals: 2,
  maxIterations: 10,
});

const repairResult = repairer.repair(plan, validationResult);
if (repairResult.success) {
  console.log('Repaired plan:', repairResult.repairedPlan);
} else {
  console.log('Suggestions:', repairResult.suggestions);
}

Main Orchestrator

The NeuroSymbolic class integrates all modules.

import { createNeuroSymbolic } from '@cogitator-ai/neuro-symbolic';

const ns = createNeuroSymbolic({
  graphAdapter: myGraphAdapter, // Optional: for knowledge graph queries
  config: {
    knowledgeGraph: {
      enableNaturalLanguage: true,
      defaultQueryLimit: 100,
    },
    logic: {
      maxDepth: 50,
      maxSolutions: 10,
      timeout: 5000,
    },
    constraints: {
      timeout: 10000,
      solver: 'z3', // or 'simple-sat'
    },
    planning: {
      maxPlanLength: 100,
      enableRepair: true,
      verifyInvariants: true,
    },
  },
});

// Logic
ns.loadLogicProgram('...');
const logicResult = ns.queryLogic('...');

// Constraints
const solverResult = await ns.solve(problem);

// Knowledge Graph
const graphResult = await ns.queryGraph(query);
const nlResult = await ns.askGraph('natural language question');

// Planning
ns.registerAction(actionSchema);
const validationResult = await ns.validatePlan(plan);
const repairResult = await ns.repairPlan(plan, validationResult);

Module Imports

Each module can be imported separately:

// Logic Programming
import {
  KnowledgeBase,
  SLDResolver,
  parseQuery,
  formatSolutions,
} from '@cogitator-ai/neuro-symbolic/logic';

// Knowledge Graph
import {
  GraphQueryBuilder,
  executeQuery,
  ReasoningEngine,
} from '@cogitator-ai/neuro-symbolic/knowledge-graph';

// Constraints
import { ConstraintBuilder, solve, Z3WASMSolver } from '@cogitator-ai/neuro-symbolic/constraints';

// Planning
import {
  ActionSchemaBuilder,
  PlanValidator,
  InvariantChecker,
} from '@cogitator-ai/neuro-symbolic/planning';

Type Reference

import type {
  // Logic
  Term,
  Clause,
  Substitution,
  ProofTree,
  LogicQueryResult,

  // Knowledge Graph
  GraphQuery,
  GraphQueryResult,
  NaturalLanguageQueryResult,

  // Constraints
  ConstraintProblem,
  ConstraintVariable,
  SolverResult,

  // Planning
  ActionSchema,
  Plan,
  PlanState,
  PlanValidationResult,
  SafetyProperty,
  InvariantCheckResult,
} from '@cogitator-ai/types';

License

MIT