LLMs describe.
Euclid proves.

Your agent is guessing. Make it prove its answers.

LLMs process information statistically, not logically. Ask one to evaluate access policies across hundreds of records and it hallucinates systematically — wrong counts, missed conflicts, fabricated permissions. For rules that matter, "approximately correct" isn't correct.

Up and running in two minutes

pip install euclid-mcp           # MCP server + CLI/REPL — pure Python, works out of the box

# Suggested for best performance (optional): without it, a built-in pure-Python engine takes over.
brew install swi-prolog          # apt install swi-prolog · choco install swi-prolog

{
  "mcpServers": {
    "euclid-mcp": { "command": "euclid-mcp" }
  }
}

$ euclid-cli
Euclid-MCP REPL — type facts and rules in Euclid-IR, then `? query`.
euclid > human(socrates)
euclid > mortal($x) IF human($x)
euclid > ? mortal($who)
Solution 1:
  who: socrates
mortal(socrates)  [rule]
  human(socrates)  [fact]

# Start the API server once — from a clone:
git clone https://github.com/meob/Euclid-MCP && cd Euclid-MCP
python3 integrations/euclid_api.py --port 8080
# …or with Docker (bundles SWI-Prolog): docker compose up euclid-api

# …then call it:
curl -X POST http://localhost:8080/reason \
  -H "Content-Type: application/json" \
  -d '{"knowledge": "human(socrates)\nmortal($x) IF human($x)\n? mortal($who)"}'

How it works

The LLM never reasons — it only describes. All deduction happens outside the model, which is why a local 8B model can outperform 400B+ cloud models on reasoning tasks.

• The LLM translates the problem into facts, rules, and a query in Euclid-IR.
• A persistent SWI-Prolog engine executes the deduction (JSON-lines protocol, no per-call spawn overhead).
• Solutions come back with variable bindings and full proof trees — or a diagnosis of why the query fails.
• No SWI-Prolog available? A pure-Python native engine interprets Euclid-IR directly, byte-identical semantics.

Euclid-IR — logic without the Prolog syntax

A declarative intermediate representation designed for both humans and LLMs: variables start with $, implication is IF, conjunction is AND.

# Facts
parent(tom, bob)
parent(bob, ann)

# Rules (recursion is fine)
ancestor($x, $y) IF parent($x, $y)
ancestor($x, $y) IF parent($x, $z) AND ancestor($z, $y)

# Audit-trail ID on any rule
can_deploy($user) IF
    user($user) AND
    has_role($user, deployer)  # RULE: DEPLOY-POL-1

# Arithmetic & negation
stale($u) IF last_login($u, $d) AND $d > 90
blocked($u) IF NOT active($u)

# Query
? ancestor(tom, $who)

{
  "query": "ancestor(tom, $who)",
  "solutions": [
    {
      "substitutions": { "who": "bob" },
      "proof": {
        "type": "rule",
        "goal": "ancestor(tom, bob)",
        "rule_id": null,
        "subproof":
          { "type": "fact",
            "goal": "parent(tom, bob)" }
      }
    },
    { "substitutions": { "who": "ann" }, "proof": { … } }
  ],
  "elapsed_ms": 12.4,
  "content_hash": "a3f9c1e4…"
}

Eight tools, one purpose

Not just deduction — a complete lifecycle: validate, reason, explain, diagnose, explore scenarios.

Load the rules once. Query them forever.

Complex business rules don't belong in a prompt. Preload a KB at server startup (EUCLID_KB_PATH) or register it under a kb_id — then each request carries only session-specific facts via delta_knowledge. Small models can reason over large rule sets without ever seeing the whole thing.

See it in action

Real euclid-cli sessions, unedited. Facts in, proof trees out — every step deterministic, every conclusion auditable.

Multi-hop RBAC

Who can deploy to production? Roles, clearance levels and an arithmetic check chained into one derivation — with the full proof tree.

Diagnose & what-if

bob is denied. Why not? The diagnosis pinpoints the gap, and a hypothetical role grant flips the answer from 0 to 1 solution.

Negation as failure

SEC-042 denies the vault to suspended users. carol fails, dave passes — and the explanation cites the rule by ID for audit.

An 8B model beats a 480B cloud model

Large-scale RBAC task over 1,000+ facts with role hierarchies and separation-of-duties constraints. Both LLMs alone fail systematically; the 8B model augmented with Euclid-MCP answers everything, faster and cheaper.

On small tasks (5–50 facts) all configurations score 5/5 — scale is where probabilistic reasoning breaks. Full methodology: benchmark reports.

Built for rules that matter

Consume it your way