# 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

```bash
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](https://www.swi-prolog.org/Download.html) |

Check that the backend is visible:

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

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

```json
{
  "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.

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

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

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

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

```bash
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`](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`](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.

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

```bash
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`](SPEC.md),
[`CLAUDE.md`](CLAUDE.md) and [`specs/`](specs/).

## License

MIT. See [LICENSE](LICENSE).