@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

Z3 SMT support is an optional dependency. If it is not installed automatically, add it explicitly:

pnpm add z3-solver

Without Z3 the package falls back to the built-in solver (exact search for finite domains, local search otherwise).

The Postgres and Neo4j graph adapters need their drivers (optional peer dependencies):

pnpm add pg            # createPostgresGraphAdapter
pnpm add neo4j-driver  # createNeo4jGraphAdapter

Website docs: Neuro-Symbolic.

Features

• Logic Programming - Prolog engine with ISO operator precedence, cut, if-then-else, negation, findall/3, between/3 and proof trees
• Knowledge Graph Queries - SPARQL-like query language, natural language questions, path finding and rule-based inference
• Constraint Solving - SAT/SMT solving with Z3 (WASM) or a pure-TS fallback, including optimisation and soft constraints
• Plan Verification - PDDL-like action schemas with validation, ordering-threat detection, invariant checking and automatic repair

Quick Start

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

const ns = createNeuroSymbolic();

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.data?.solutions[0].get('X')); // { type: 'atom', value: 'ann' }
console.log(ns.getLogicSolutions('grandparent(tom, X)')); // "X = ann."

const builder = ns.createConstraintProblem('sum');
const x = builder.int('x', 1, 10);
const y = builder.int('y', 1, 10);
builder.assert(x.add(y).eq(15));
builder.maximize(x);

const solution = await ns.solve(builder.build());
if (solution.data?.status === 'sat') {
  console.log(solution.data.model.assignments); // { x: 10, y: 5 }
}

Logic Programming

Prolog-style logic programming with SLD resolution, unification and standard operator syntax.

Loading Programs

ns.loadLogicProgram(`
  % Facts
  human(socrates).
  human(plato).

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

  % Arithmetic uses ISO precedence: * binds tighter than +
  total(Price, Qty, T) :- T is Price * Qty + 5.

  % Cut is local to the clause that executes it
  grade(S, a) :- S >= 90, !.
  grade(S, b) :- S >= 75, !.
  grade(_, c).

  % If-then-else commits to the condition
  label(S, L) :- ( S >= 50 -> L = pass ; L = fail ).
`);

loadLogicProgram returns { success, errors }; syntax errors include the line and column.

Querying

Queries may be written with or without a trailing ./? and an optional ?- prefix.

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

ns.proveLogic('mortal(socrates)').data; // true
ns.getLogicSolutions('append(X, Y, [1, 2])');
// "X = [], Y = [1, 2] ;\nX = [1], Y = [2] ;\nX = [1, 2], Y = []."

ns.queryLogic('findall(X, human(X), L), length(L, N)', { maxSolutions: 1 });

Variables starting with _ (including the anonymous _) are not reported in answers. When a query runs out of time or depth, result.error / result.data.explanation says so.

Proof Trees

Enable traceExecution to capture the proof tree:

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

const traced = createNeuroSymbolic({ config: { logic: { traceExecution: true } } });
traced.loadLogicProgram(
  'parent(tom, mary). parent(mary, ann). grandparent(X, Z) :- parent(X, Y), parent(Y, Z).'
);

const proof = traced.queryLogic('grandparent(tom, X)').data?.proofTree;
if (proof) {
  console.log(formatProofTree(proof));
  console.log(proofTreeToMermaid(proof));
}

Built-in Predicates

Arithmetic follows ISO semantics (-7 mod 3 =:= 2, -7 // 2 =:= -3, div, bitwise /\ \/ xor << >>, gcd, min, max, abs, trigonometry, pi, e, ...). Undefined results such as sqrt(-1) fail instead of binding NaN. Use getBuiltinList() / isControlConstruct() to inspect support at runtime.

Knowledge Graph Queries

SPARQL-like query language with natural language interface. Works with any GraphAdapter (in-memory, Postgres, Neo4j, or adapters from @cogitator-ai/memory).

Query Builder

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

const query = GraphQueryBuilder.select()
  .where(variable('person'), 'works_at', variable('company'))
  .where(variable('company'), 'located_in', 'Berlin')
  .filter('person.name', 'startsWith', 'A')
  .orderBy('person.name', 'asc')
  .limit(10)
  .build();

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

• Patterns join on shared variables; bidirectional edges match in both directions.
• ?x a person / ?x type person matches node entity types.
• describe queries match edges in either direction around the subject.
• Filters can address nested properties: person.properties.profile.level.
• count('*', 'total') counts all bindings.

Query Strings

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

const parsed = parseQueryString(`
  SELECT ?p WHERE { ?p works_at ?c . ?c located_in Berlin }
  FILTER(?p.confidence >= 0.5)
  ORDER BY DESC(?p.name)
  LIMIT 5
`);

Supported filter operators: = != > >= < <= contains startsWith endsWith regex in notIn.

Natural Language Queries

const answer = await ns.askGraph('Who works at "Acme"?');
console.log(answer.data?.naturalLanguageResponse);

NeuroSymbolic honours config.knowledgeGraph.enableNaturalLanguage and applies defaultQueryLimit to queries without an explicit limit.

Reasoning Engine

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

const engine = createReasoningEngine(graphAdapter, 'agent-1', { maxHops: 3, minConfidence: 0.5 });

const path = await engine.findPath(aliceId, companyId);
const hops = await engine.multiHopQuery(aliceId, ['works_at', 'located_in']);
const inferred = await engine.infer(); // transitive, inverse and composed relations, de-duplicated

Constraint Solving

SAT/SMT solving with a fluent DSL. Variable declarations return expressions; constraints are added to the builder.

Building Constraints

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

const builder = ConstraintBuilder.create('example');
const a = builder.bool('a');
const b = builder.bool('b');
const x = builder.int('x', 0, 100);
const y = builder.int('y', 0, 100);
const z = builder.real('z', 0, 1);

builder.assert(a.or(b));
builder.assert(x.add(y).lte(50));
builder.assert(z.mul(2).gt(0.5));
builder.assert(allDifferent(x, y));
builder.soft(x.eq(10), 2);
builder.maximize(x.add(y));

const result = await solve(builder.build());
if (result.status === 'sat') {
  console.log(result.model.assignments, result.model.objectiveValue);
}

Declaring the same variable twice or an empty domain (min > max) throws.

Solver Selection

solve(problem, { solver: 'z3' }) (the default) uses Z3 when z3-solver can be loaded and otherwise falls back to the built-in solver.

import { isZ3Available, solveWithZ3, solveSAT } from '@cogitator-ai/neuro-symbolic';

const result = (await isZ3Available()) ? await solveWithZ3(problem) : solveSAT(problem);

• Z3: integers, reals, booleans and bit-vectors (unsigned semantics); mixed Int/Real expressions are coerced automatically; objectives and soft constraints use Z3's optimiser.
• Built-in solver: exhaustive search when every variable has a finite domain (≤ 2^20 assignments) — exact sat/unsat, optimal objective, minimal soft-constraint violations; local search for real or unbounded variables (may return unknown).

Expression Types

x.add(y);
x.sub(5);
x.mul(2);
x.div(3);
x.mod(7);
x.pow(2);
x.abs();
x.min(y);
x.max(y);
a.and(b);
a.or(b);
a.not();
a.implies(b);
a.iff(b);
x.eq(10);
x.neq(y);
x.gt(0);
x.gte(0);
x.lt(100);
x.lte(100);

ite(a, x, y);
sum(x, y, z);
allDifferent(x, y, z);
atMost(2, a, b, c);
atLeast(1, a, b, c);
exactly(1, a, b, c);

Plan Verification

PDDL-like planning with verification and repair. Parameter references use the ?name syntax.

Action Schemas

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

const move = ActionSchemaBuilder.create('move')
  .describe('Move robot from one location to another')
  .param('from', 'string')
  .param('to', 'string')
  .preSimple('robotAt', '?from')
  .preCompare('battery', 'gt', 10)
  .assign('robotAt', '?to')
  .decrement('battery', 5)
  .setCost(5)
  .build();

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

Precondition equality is structural (arrays and objects compare by value). Conditional effects evaluate their condition against the state before the action.

Plan Validation

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

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

const result = validatePlan(plan, registry, { maxSteps: 50 });
console.log(formatValidationResult(result));

Validation reports precondition violations, missing/unknown parameters, unmet goals, redundant actions and ordering threats (an action deleting a variable a later action requires).

Invariant Checking

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

const checker = createInvariantChecker(registry);
checker.addInvariant('battery-non-negative', {
  type: 'comparison',
  variable: 'battery',
  operator: 'gte',
  value: 0,
});
checker.addNever('danger', { type: 'simple', variable: 'robotAt', value: 'danger-zone' });
checker.addEventually('arrived', { type: 'simple', variable: 'robotAt', value: 'C' });

console.log(formatInvariantResults(checker.checkPlan(plan)));

The trajectory stops at the first action whose preconditions do not hold.

Plan Repair

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

const repairer = createPlanRepairer(registry, { maxInsertions: 3, maxRemovals: 2 });
const repair = repairer.repair(plan);

if (repair.success) {
  console.log('Repaired plan:', repair.repairedPlan);
} else {
  console.log(formatRepairResult(repair));
}

Insertion suggestions are verified by simulation (an action is only suggested if applying it establishes the failed condition); missing parameters are filled from defaults or the current state.

Main Orchestrator

The NeuroSymbolic class integrates all modules. Every method returns a NeuroSymbolicResult ({ success, data?, error?, duration }) instead of throwing.

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

const ns = createNeuroSymbolic({
  graphAdapter: myGraphAdapter,
  agentId: 'agent-1',
  config: {
    knowledgeGraph: { enableNaturalLanguage: true, defaultQueryLimit: 100 },
    logic: { maxDepth: 50, maxSolutions: 10, timeout: 5000 },
    constraints: { timeout: 10000, solver: 'z3' },
    planning: { maxPlanLength: 100, enableRepair: true, verifyInvariants: true },
  },
});

ns.loadLogicProgram('...');
ns.queryLogic('...');

await ns.solve(problem);

await ns.queryGraph(query);
await ns.askGraph('natural language question');
await ns.findPath(startNodeId, endNodeId);

ns.registerAction(actionSchema);
ns.validatePlan(plan);
ns.repairPlan(plan);
ns.checkInvariants(plan);
await ns.validateAndRepair(plan);

ns.getConfig() returns a ResolvedNeuroSymbolicConfig: every section (logic, constraints, planning, knowledgeGraph) is present with its defaults filled in, so no optional chaining is needed. ns.updateConfig(partial) merges changes into the running instance.

const { logic, constraints } = ns.getConfig();
console.log(logic.maxDepth, constraints.timeout);

ns.updateConfig({ logic: { maxSolutions: 5 } });

Agent Tools

Expose neuro-symbolic capabilities as tools for AI agents.

import { createNeuroSymbolicTools, MemoryGraphAdapter } from '@cogitator-ai/neuro-symbolic';
import { Agent, Cogitator } from '@cogitator-ai/core';

const nsTools = createNeuroSymbolicTools({ graphAdapter: new MemoryGraphAdapter() });

nsTools.instance.loadLogicProgram(`
  parent(tom, mary).
  parent(mary, ann).
  grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
`);

const agent = new Agent({
  name: 'reasoning-agent',
  model: 'openai/gpt-6.1-sol',
  tools: nsTools.all,
  instructions:
    'Use query_logic for Prolog queries, solve_constraints for SAT/SMT problems and validate_plan to verify action sequences.',
});

const cogitator = new Cogitator({
  llm: { providers: { openai: { apiKey: process.env.OPENAI_API_KEY! } } },
});
const result = await cogitator.run(agent, { input: 'Who are the grandparents of ann?' });

Available Tools

*Graph tools are available when a graphAdapter is passed or the provided instance has one.

Factory Options

interface NeuroSymbolicToolsOptions {
  instance?: NeuroSymbolic;
  graphAdapter?: GraphAdapter;
  config?: Partial<NeuroSymbolicConfig>;
  agentId?: string;
}

When agentId is set, graph tools read and write that agent's graph; otherwise they use the calling agent's id from the tool context. createGraphTools(adapter, { agentId }) can be used on its own.

Graph Adapters

import {
  MemoryGraphAdapter,
  createPostgresGraphAdapter,
  createNeo4jGraphAdapter,
} from '@cogitator-ai/neuro-symbolic';

const memory = new MemoryGraphAdapter();
await memory.addNode({
  agentId: 'agent-1',
  name: 'Alice',
  type: 'person',
  aliases: [],
  properties: { age: 30 },
  confidence: 1,
  source: 'user',
});

const postgres = createPostgresGraphAdapter({ connectionString: process.env.DATABASE_URL! });
await postgres.connect();

const neo4j = createNeo4jGraphAdapter({
  uri: 'bolt://localhost:7687',
  username: 'neo4j',
  password: 'secret',
});
await neo4j.connect();

All adapters scope traversal and shortest-path search to the requesting agent, treat bidirectional edges as traversable in both directions and reject merges into a node listed among its own sources.

The Postgres adapter uses the pgvector extension for searchNodesSemantic(). It indexes node embeddings with HNSW, which needs no training data, so the index built on the empty table finds every node as the graph grows. Earlier versions built an ivfflat index there, which missed nodes once Postgres used it (a search for 60 nodes in a graph of 3000 returned 31). The first connect() after upgrading replaces that index with HNSW, which takes a while on a large graph. To avoid the wait, build the index ahead of the deploy with CREATE INDEX CONCURRENTLY idx_graph_nodes_embedding_new ON cogitator_graph.graph_nodes USING hnsw (embedding vector_cosine_ops), then drop the old index and rename the new one to idx_graph_nodes_embedding. An existing HNSW index is kept as it is. Each search raises hnsw.ef_search to the requested limit (up to 1000) and, on pgvector 0.8 or later, turns on iterative scans, so a large limit or an entityTypes filter still gets every matching node. Equally similar nodes are ordered by id.

Module Imports

Each module can be imported separately:

import {
  KnowledgeBase,
  SLDResolver,
  parseQuery,
  formatSolutions,
} from '@cogitator-ai/neuro-symbolic/logic';
import {
  GraphQueryBuilder,
  executeQuery,
  ReasoningEngine,
} from '@cogitator-ai/neuro-symbolic/knowledge-graph';
import { ConstraintBuilder, solve, Z3WASMSolver } from '@cogitator-ai/neuro-symbolic/constraints';
import {
  ActionSchemaBuilder,
  PlanValidator,
  InvariantChecker,
} from '@cogitator-ai/neuro-symbolic/planning';
import { createNeuroSymbolicTools } from '@cogitator-ai/neuro-symbolic/tools';

Type Reference

import type {
  Term,
  Clause,
  Substitution,
  ProofTree,
  LogicQueryResult,
  GraphQuery,
  GraphQueryResult,
  NaturalLanguageQueryResult,
  ConstraintProblem,
  ConstraintVariable,
  SolverResult,
  ActionSchema,
  Plan,
  PlanState,
  PlanValidationResult,
  SafetyProperty,
  InvariantCheckResult,
} from '@cogitator-ai/types';

License

MIT