Combine neural LLM reasoning with Prolog-style logic, SAT/SMT constraint solving, knowledge graph queries and verified planning.

Overview

Pure LLM reasoning excels at natural language understanding but struggles with strict logical constraints, guaranteed correctness and systematic search. @cogitator-ai/neuro-symbolic bridges this gap: the LLM formulates problems in symbolic terms, a symbolic engine solves them exactly, and the LLM explains the result.

pnpm add @cogitator-ai/neuro-symbolic
pnpm add z3-solver # optional, enables the Z3 SMT backend

The package has four modules, all reachable through the NeuroSymbolic orchestrator or as standalone imports:

Module	What it does
Logic	Prolog engine: ISO operators, cut, if-then-else, negation, `findall/3`, proof trees
Constraints	SAT/SMT via Z3 (WASM) or a built-in solver, with optimisation and soft constraints
Knowledge graph	SPARQL-like queries, natural language questions, path finding and rule inference
Planning	Action schemas, plan validation, ordering-threat detection, invariants, plan repair

Agent Tools

The fastest way to give an agent formal reasoning is createNeuroSymbolicTools:

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

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

tools.instance.loadLogicProgram(`
  parent(tom, bob). parent(bob, ann). parent(bob, pat).
  grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
`);

const agent = new Agent({
  name: 'reasoner',
  model: 'google/gemini-3.8-flash',
  instructions:
    'Answer family questions by calling query_logic. Use solve_constraints for scheduling and validate_plan to verify action sequences.',
  tools: tools.all,
});

const cog = new Cogitator({ llm: { defaultModel: 'google/gemini-3.8-flash' } });
const result = await cog.run(agent, { input: 'Who are the grandchildren of tom?' });

Tool	Purpose
`query_logic`	Run a Prolog query against the knowledge base
`assert_fact`	Add facts or rules
`load_logic_program`	Load a whole program (optionally clearing)
`solve_constraints`	Solve a CSP with an optional objective
`validate_plan`	Validate a plan against registered actions
`repair_plan`	Repair an invalid plan
`register_action`	Register an action schema
`find_graph_path`	Shortest path between graph nodes (graph only)
`query_graph`	Query graph nodes and edges (graph only)
`add_graph_node`	Add a node (graph only)
`add_graph_edge`	Add an edge (graph only)

Graph tools are added when a graphAdapter is passed or the supplied instance has one. Pass agentId to pin graph tools to a specific graph instead of the calling agent's id.

Logic Programming

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

const ns = createNeuroSymbolic();

ns.loadLogicProgram(`
  price(laptop, 1200). price(mouse, 25). price(monitor, 300).

  discount(Total, D) :- ( Total >= 1000 -> D is Total * 0.1 ; D = 0 ).

  tier(P, premium) :- P >= 1000, !.
  tier(P, standard) :- P >= 100, !.
  tier(_, budget).
`);

ns.getLogicSolutions('findall(P, price(_, P), Ps), sum_list(Ps, T), discount(T, D)');
// "Ps = [1200, 25, 300], T = 1525, D = 152.5."

ns.getLogicSolutions('price(mouse, P), tier(P, Tier)?');
// "P = 25, Tier = budget."

Operators follow ISO precedence (X is 2 + 3 * 4 gives 14), mod/// follow ISO semantics.
Cut is local to its clause; ( C -> T ; E ) commits to the first solution of C.
Control constructs: \+, not/1, call/N, findall/3, forall/2, between/3.
Queries may end with . or ?; _-prefixed variables are not reported.
Set config.logic.traceExecution = true to get a proof tree (formatProofTree, proofTreeToMermaid).
getLogicSolutions returns the solutions as text; queryLogic(query, { maxSolutions }) returns them as data and proveLogic(query) as a boolean. assertFact('parent', 'tom', 'bob') adds a single fact.
Resolution is bounded by config.logic (defaults: maxDepth 50, maxSolutions 10, timeout 5000 ms): createNeuroSymbolic({ config: { logic: { maxSolutions: 100 } } }).

Constraint Solving

const problem = ns.createConstraintProblem('staffing');
const seniors = problem.int('seniors', 0, 10);
const juniors = problem.int('juniors', 0, 10);

problem.assert(seniors.add(juniors).gte(8));
problem.assert(seniors.mul(2).gte(juniors));
problem.minimize(seniors.mul(300).add(juniors.mul(180)));

const result = await ns.solve(problem.build());
if (result.data?.status === 'sat') {
  console.log(result.data.model.assignments); // { seniors: 3, juniors: 5 }
}

With solver: 'z3' (the default) the Z3 backend is used whenever z3-solver loads; it supports ints, reals (mixed expressions are coerced), booleans and unsigned bit-vectors, plus minimize/maximize and weighted soft() constraints. Without Z3 the built-in solver searches finite domains exhaustively (exact sat/unsat and optimal objectives) and falls back to local search for real or unbounded variables.

Knowledge Graph Queries

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

const graph = new MemoryGraphAdapter();
const kg = createNeuroSymbolic({ graphAdapter: graph, agentId: 'demo' });

const berlin = await kg.queryGraph(
  parseQueryString('SELECT ?p WHERE { ?p works_at ?c . ?c located_in Berlin } ORDER BY ?p.name')
);

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

Patterns join on shared variables, bidirectional edges match in both directions, ?x a person matches node types and FILTER, ORDER BY, LIMIT, OFFSET are supported. createReasoningEngine(adapter, agentId) adds shortest paths, multi-hop relation chains and de-duplicated transitive / inverse / compositional inference. Postgres and Neo4j adapters are available via createPostgresGraphAdapter and createNeo4jGraphAdapter. The Postgres adapter indexes node embeddings with HNSW (pgvector), so semantic search finds every node from the first insert on, and raises hnsw.ef_search to the requested limit. Earlier versions built an ivfflat index on the empty table that missed nodes. The first connect() after upgrading replaces it, see the package README for building the new index ahead of a deploy on a large graph.

Verified Planning

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

ns.registerActions([
  ActionSchemaBuilder.create('charge').assign('battery', 100).build(),
  ActionSchemaBuilder.create('fly')
    .param('to', 'string')
    .preCompare('battery', 'gte', 50)
    .assign('location', '?to')
    .decrement('battery', 50)
    .build(),
]);

ns.addSafetyProperty({
  id: 'battery-floor',
  name: 'battery never negative',
  type: 'invariant',
  condition: { type: 'comparison', variable: 'battery', operator: 'gte', value: 0 },
});

const outcome = await ns.validateAndRepair({
  id: 'delivery',
  initialState: { id: 's0', variables: { battery: 10, location: 'base' } },
  actions: [createAction('fly', { to: 'depot' })],
  goalConditions: [{ type: 'simple', variable: 'location', value: 'depot' }],
});

outcome.data?.finalPlan.actions.map((a) => a.schemaName); // ['charge', 'fly']
outcome.success; // true: the repaired plan is valid and every invariant holds

Validation reports precondition violations, parameter errors, unmet goals, redundant actions and ordering threats. Repair suggestions are verified by simulation before they are proposed.

LLM Prompt Helpers

Each module ships prompt builders and robust response parsers for the neural half of the loop, for example createNLToFactsPrompt + parseLLMFactsResponse (text to Prolog facts), createNLToConstraintsPrompt + parseNLConstraintsResponse, createPlanGenerationPrompt + parsePlanResponse, and createEntityExtractionPrompt + parseEntityExtractionResponse. Parsers validate LLM output and drop malformed entries instead of throwing.

Neuro-Symbolic AI

Overview

Agent Tools

Logic Programming

Constraint Solving

Knowledge Graph Queries

Verified Planning

LLM Prompt Helpers

On this page

Neuro-Symbolic AI

OverviewCopy Anchor Link

Agent ToolsCopy Anchor Link

Logic ProgrammingCopy Anchor Link

Constraint SolvingCopy Anchor Link

Knowledge Graph QueriesCopy Anchor Link

Verified PlanningCopy Anchor Link

LLM Prompt HelpersCopy Anchor Link

On this page

Overview

Agent Tools

Logic Programming

Constraint Solving

Knowledge Graph Queries

Verified Planning

LLM Prompt Helpers