# Neuro-Symbolic AI

URL: https://cogitator.app/docs/advanced/neuro-symbolic

> 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.

```bash
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`:

```typescript
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

```typescript
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

```typescript
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

```typescript
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

```typescript
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.