Euclid-MCP

Deterministic logical reasoning for MCP clients, with proof trees.

Reference implementation of Euclid-MCP: A Model Context Protocol Server for Deterministic Logical Reasoning via Prolog (Bogliolo, arXiv:2607.21412v1).

An LLM is good at describing a world and bad at deducing over it. Euclid-MCP splits those jobs: the model writes facts, rules and a query in a small declarative language (Euclid-IR); the server compiles that to Prolog, runs it in a sandboxed subprocess, and returns exact answers with a derivation for every one of them. On a 1,000-user RBAC knowledge base where natural-language reasoning hallucinates counts, this returns 31 and 103 — every time, with the proof attached.

┌────────────┐   Euclid-IR    ┌──────────────────────────────┐   Prolog    ┌────────────┐
│ LLM client │ ─────────────▶ │        Euclid-MCP server     │ ──────────▶ │ SWI-Prolog │
│ (MCP)      │                │  parse → lower → sanitize →  │  (subproc)  │  (deduce)  │
│            │ ◀───────────── │  run → parse JSON → typed    │ ◀────────── │            │
└────────────┘  solutions +   │  result                      │  JSON       └────────────┘
                proof trees   └──────────────────────────────┘

---

Install

pip install euclid-mcp

SWI-Prolog is a system dependency, not a pip dependency. You need swipl 9.0 or later on PATH:

Platform	Command
Debian/Ubuntu	apt-get install -y swi-prolog
macOS	brew install swi-prolog
Fedora	dnf install pl
Windows	swi-prolog.org/download

Check that the backend is visible:

python -m euclid_mcp --check
# euclid-mcp 0.1.0
# backend: SWI-Prolog version 9.0.4 for x86_64-linux

Or skip the install entirely and use the Docker image, which bundles SWI-Prolog:

docker build -t euclid-mcp .
docker run --rm -p 8000:8000 euclid-mcp
curl -s localhost:8000/health

Connect an MCP client

python -m euclid_mcp speaks MCP over stdio. For Claude Desktop, Cursor, or any other MCP client, add:

{
  "mcpServers": {
    "euclid": {
      "command": "python",
      "args": ["-m", "euclid_mcp"]
    }
  }
}

Euclid-IR in one screen

One logical item per line. Predicates and constants are lowercase; variables start with $.

@version 1.0                                    # optional directive

parent(tom, bob)                                # a fact - must be ground
parent(bob, ann)

mortal($x) IF human($x)                         # a rule
ancestor($x, $y) IF parent($x, $y)
ancestor($x, $y) IF parent($x, $z) AND          # continues: line ends in AND
    ancestor($z, $y)

blocked($u) IF NOT active($u)                   # closed-world negation
stale($u) IF last_login($u, $d) AND $d > 90     # arithmetic comparison
resource(apple, $color, _, _, _, _)             # _ is a wildcard

? ancestor(tom, $who)                           # a query

Comparison operators: > >= < =< =:= =\= is. Comments: # or //, whole-line or inline.

There is also an equivalent YAML form; both load into the same AST.

version: "1.0"
facts:
  - parent(tom, bob)
rules:
  - head: ancestor($x, $y)
    body: [ parent($x, $y) ]
queries:
  - ? ancestor(tom, $who)

Deliberately not supported

Not supported	Do this instead
disjunction (OR, ;)	write several rules with the same head
lists [...]	model a collection as several facts
strings	use lowercase atoms
cut !	nothing — proofs are always complete
findall / bagof / setof	precompute counts as facts (permission_count(u, 17))
runtime assert / retract	use the what_if tool
modules	—

These restrictions are the point: they keep every proof finite, traceable and reproducible, and they keep the language portable to a second backend. Each one is rejected at parse time with a message that names the construct and the workaround.

The four tools

All four are stateless and read-only: knowledge in, typed result out.

Tool	Purpose
reason	Prove a goal; return every solution with its proof tree
diagnose	Explain a result: why, why_not, what_needs
what_if	Apply +/- fact changes and diff the before/after solutions
check_kb	Static validation — syntax, undefined predicates, cycles, duplicates

They are designed around a translate-run-inspect-repair loop:

1. Validate — check_kb confirms the knowledge base is well-formed (no backend needed, so it is cheap).
2. Translate — the client emits Euclid-IR: facts, rules, query.
3. Run — reason returns answers plus derivations.
4. Inspect — on a surprising result, diagnose with why or why_not.
5. Repair — refine the knowledge base from the diagnosis; re-run.
6. Explore — what_if tests a hypothetical change before committing to it.

Every failure — a parse error, an unsupported construct, an oversized payload, a timeout — comes back as ok: false with an actionable message rather than an exception, so the client can correct itself and retry.

reason

reason(knowledge="""
parent(tom, bob)
parent(bob, ann)
ancestor($x, $y) IF parent($x, $y)
ancestor($x, $y) IF parent($x, $z) AND ancestor($z, $y)
""", query="ancestor(tom, $who)")

solution_count: 2, truncated: false
  $who = ann
    ancestor(tom, ann)  [rule]
      parent(tom, bob)  [fact]
      ancestor(bob, ann)  [rule]
        parent(bob, ann)  [fact]
  $who = bob
    ancestor(tom, bob)  [rule]
      parent(tom, bob)  [fact]

An empty solutions list with ok: true is a real answer: under closed-world semantics the knowledge base does not entail the goal.

diagnose

diagnose(knowledge="human(socrates)", query="mortal(plato)", mode="why_not")
# holds: false
# findings: ["No facts or rules defined for 'mortal'"]
# conclusion: The knowledge base defines nothing for `mortal`, so any goal that
#             depends on it fails. Add the missing facts or a rule whose head uses it.

what_needs goes further and abduces the repair: given mortal($x) IF human($x) it answers that adding human(plato) would make the goal hold.

what_if

what_if(base_knowledge=rbac_kb,
        modifications="- has_role(eng_0002, intern)\n+ has_role(eng_0002, senior_dev)",
        query="user_has_permission(eng_0002, deploy_code)")
# before_count: 0, after_count: 1, delta: 1

A - line that matches no existing fact is an error, not a silent no-op: a scenario built on a false premise would give a misleading answer.

REST API

For automation platforms (n8n, Zapier, Make) and remote access. The endpoints call the same tool functions with the same Pydantic models — one schema, two surfaces.

python -m euclid_mcp --http --host 0.0.0.0 --port 8000

Method	Path	Body	Response
POST	/reason	ReasonInput	ReasonResult
POST	/diagnose	DiagnoseInput	DiagnosisResult
POST	/what-if	WhatIfInput	WhatIfResult
POST	/check-kb	CheckKBInput	KBCheckResult
GET	/health	—	{"status": "ok", "swipl": "...", "version": "..."}

OpenAPI docs are at /docs. CORS is off by default; set EUCLID_MCP_CORS_ORIGINS to a comma-separated origin list (or *) to enable it for browser clients.

Do not expose this API to an untrusted network as-is. There is no authentication, authorization or rate limiting, and nothing caps concurrent work. Every request spawns a reasoning subprocess that may run for the full 30 s timeout — and what_if and diagnose each run the backend twice, so one request can buy ~60 s of CPU. A handful of small requests will saturate every core. The CLI binds loopback by default; the container image binds 0.0.0.0.

Put a reverse proxy in front of it providing auth, rate limiting and a concurrency cap, or keep it on a trusted network. See THREATMODEL.md finding F4.

Safety

The LLM cannot make the backend do anything but deduce.

• Size cap — knowledge over 500 KB is rejected before parsing.
• Time bound — every program runs under a 30 s wall clock, enforced both by the subprocess and by call_with_time_limit/2 inside Prolog.
• Allow-list — only constructors reachable from the grammar can be emitted. File I/O, network, shell, consult, use_module and runtime assert/retract are unreachable from Euclid-IR and rejected if they somehow appear.
• Generated-text audit — the lowered program is scanned for denied built-ins before it runs, so a lowering bug cannot smuggle one through.
• In-Prolog verification — before executing anything, the harness walks every clause body and refuses to run if it finds a goal that is not a declared knowledge-base predicate, a comparison, or a negation of those.
• No shell=True, argv lists only, temp files removed in a finally.

What is not defended

Read THREATMODEL.md before deploying. In short:

• Soundness is relative to the encoded rules, not to reality. The model writes the knowledge base; wrong premises yield wrong conclusions with valid proofs. The proof tree is what makes that auditable — treat the knowledge base as the security-relevant artefact and review it.
• A zero-solution answer can mean "search depth exhausted", not "false" — the two are currently indistinguishable, and the answer can flip when max_depth rises (finding F1).
• solution_count is what was returned, not what exists. Always check truncated before treating it as a total (F2).
• The REST API is unauthenticated with no rate limiting (F4, above).
• Memory is not bounded — only wall-clock time is (F5).

Determinism

Same knowledge + same query ⇒ byte-identical solution set, every run. Clauses are emitted in source order, solutions are sorted by a total order over their bindings and proofs, and nothing is seeded randomly.

Examples and benchmarks

examples/07_it_security_compliance/ is a three-layer IT-security and compliance knowledge base — CIS controls, a role hierarchy and environment/classification policy, then generated user and resource data — in a small (~30 users) and a large (~200 users) variant, so the same rules can be seen to scale unchanged.

python benchmarks/run_benchmarks.py          # accuracy + latency, exits non-zero on a miss
python benchmarks/generate_large_rbac.py     # regenerate the 1,000-user RBAC KB

evals/evaluation.xml holds ten verified question/answer pairs for MCP evaluation harnesses.

Architecture notes

The backend is a tactical choice, not an architectural dependency. ir/, tools/ and the MCP surface never mention Prolog; only lowering/ does. A Datalog or SMT backend would slot in behind the same LoweredProgram and EngineResult types.

Reasoning runs as a subprocess rather than through FFI (pyswip/MQI) for portability: no compiled extension, no persistent process, trivial to containerize. The cost is one process launch per call, roughly 30-60 ms. If that ever dominates the sub-second budget, engine/runner.py can be swapped for an MQI-backed runner behind the same signature without touching anything else.

Development

pip install -e ".[dev]"
ruff check . && ruff format --check .
mypy --strict src
pytest                      # add -m "not requires_swipl" to skip backend tests

Layout, conventions and the milestone plan are in SPEC.md, CLAUDE.md and specs/.

License

MIT. See LICENSE.