Euclid-MCP

# Euclid-MCP

[![Euclid-MCP MCP server](https://glama.ai/mcp/servers/meob/Euclid-MCP/badges/score.svg)](https://glama.ai/mcp/servers/meob/Euclid-MCP)
[![PyPI version](https://img.shields.io/pypi/v/euclid-mcp?color=blue)](https://pypi.org/project/euclid-mcp/)
[![Python versions](https://img.shields.io/pypi/pyversions/euclid-mcp)](https://pypi.org/project/euclid-mcp/)
[![License](https://img.shields.io/github/license/meob/Euclid-MCP?cacheSeconds=86400)](LICENSE)
[![CI](https://img.shields.io/github/actions/workflow/status/meob/Euclid-MCP/ci.yml?branch=main&label=CI)](https://github.com/meob/Euclid-MCP/actions/workflows/ci.yml)
[![Coverage](https://img.shields.io/codecov/c/github/meob/Euclid-MCP)](https://codecov.io/gh/meob/Euclid-MCP)

**MCP server for logical reasoning** — turns facts into formal proofs.

<!-- mcp-name: io.github.meob/euclid-mcp -->

Euclid-MCP is a hybrid cognitive architecture: a lightweight LLM describes the world in facts, and a deterministic engine performs the actual deduction. The LLM never needs to reason — it only needs to describe.

With Euclid-MCP, an 8B model can solve reasoning tasks that stump even 400B+ cloud models — because the engine handles deduction deterministically. Every answer comes with a proof tree, so you can trace *why* a conclusion holds, not just *what* it is. Use it to enforce RBAC policies, audit cloud compliance, validate loan eligibility rules, or reason over any domain where answers must be explainable and verifiable.

Euclid-MCP is written in Python and uses **Euclid-IR**, a human-readable intermediate language designed for both AI agents and humans. It uses **SWI-Prolog** as its primary inference engine — and, where SWI-Prolog is not available (e.g. minimal containers), a pure-Python **native engine** that interprets Euclid-IR directly for small knowledge bases
(see [`docs/NATIVE_ENGINE.md`](docs/NATIVE_ENGINE.md)).
It can be consumed in multiple ways: via **MCP** by AI agents (OpenCode, Claude, Cursor), via **HTTP** by tools and automation platforms (n8n, Zapier, Make), and via **Python API** for direct integration. Euclid-IR rules can also be used to **augment RAG** pipelines with deterministic policy enforcement.


## How it works

```
┌──────────────┐     ┌──────────────────┐     ┌──────────────┐     ┌─────────────────┐
│  LLM/Agent   │────▶│  Euclid-MCP      │────▶│  Translator  │────▶│  SWI-Prolog     │
│  (MCP Client)│◀────│  (MCPServer)     │◀────│  + Meta-IP   │◀────│  (persistent)   │
└──────────────┘     └──────────────────┘     └──────────────┘     └─────────────────┘
```

1. Receive facts, rules, and a query in a simple intermediate language
2. Translate into Prolog with a meta-interpreter for proof tree capture
3. Execute via a persistent SWI-Prolog engine process (JSON-lines protocol on stdin/stdout; the workspace is reloaded per call, no process spawn overhead)
4. Return solutions + proof trees as structured JSON

Additional tools (`explain`, `diagnose`, `what_if`, `check_kb`) extend this core flow with natural-language explanations, analysis, scenario testing, and validation.

LLMs describe. Euclid MCP proves.  


### Knowledge Base

For small knowledge bases, facts and rules can be provided with each request.

A knowledge base can be loaded at server startup and reused across
calls, so agents only pass the session-specific facts for the current query.
This minimizes token usage, improves performance, and allows small LLMs to reason over large rule sets without reconstructing the entire knowledge base for every request.


## Intermediate Language

Even if currently Euclid-MCP uses a Prolog Engine, no Prolog syntax is required.  
**Euclid-IR** (Intermediate Representation) is a declarative intermediate representation for logical inference.
Variables use `$name`, implication is `IF`, conjunction is `AND`.

**Text format:**
```
human(socrates)
mortal($x) IF human($x)

? mortal($who)
```

**YAML format:**
```yaml
facts:
  - parent(tom, bob)
  - parent(bob, ann)
  - parent(tom, liz)
rules:
  - ancestor($x, $y) IF parent($x, $y)
  - ancestor($x, $y) IF parent($x, $z) AND ancestor($z, $y)

query: ancestor(tom, $who)
```

Full language reference: [`docs/EUCLID_IR.md`](docs/EUCLID_IR.md)


### Euclid-IR Syntax Reference

| Element | Syntax | Example |
|---------|--------|---------|
| Facts | `predicate(args)` | `parent(tom, bob)` |
| Variables | `$name` (lowercase) | `$who`, `$x`, `$count` |
| Implication | `IF` | `mortal($x) IF human($x)` |
| Conjunction | `AND` | `p($x) AND q($x)` |
| Negation | `NOT` | `NOT active($user)` |
| Query | `? predicate` | `? ancestor(tom, $who)` |
| String literals | `"..."` or `'...'` | `"alice@example.com"` |
| Multi-line rules | Body on next line | `rule($x) IF\n    body($x)` |

### Arithmetic Comparisons

Rules support arithmetic comparisons that are evaluated during deduction:

```
# Stale access: users who haven't logged in for 90+ days
stale_access($user) IF
    user($user) AND last_login_days($user, $days) AND $days > 90

# Excessive permissions: more than 15 direct permissions
excessive_permissions($user, $count) IF
    user($user) AND permission_count($user, $count) AND $count > 15

# Clearance check: user clearance >= resource classification
can_access($user, $resource) IF
    user($user) AND resource($resource, _, _, _, _, $cls) AND
    classification($cls, $cls_level, _) AND
    user_clearance($user, $user_level) AND $user_level >= $cls_level
```

**Supported operators:** `>`, `>=`, `<`, `<=`, `==`, `is`, `!=`

### Multi-line Rules

Rules can span multiple lines for readability:

```
can_deploy($user, $env) IF
    user($user) AND
    has_role($user, $role) AND
    deploy_requires_level($env, $min) AND
    deploy_role_level($role, $level) AND
    $level >= $min AND
    user_has_permission($user, deploy_code)
```

### Conjunctions in Queries

Queries can combine multiple predicates:

```
? can_access_resource($who, $res) AND resource($res, _, _, _, _, secret)
```

This returns solutions where both conditions are satisfied simultaneously.

## Why External Inference?

The external inference gives several advantages:
- deterministic
- explainable
- verifiable
- inexpensive
- replaceable backend

In the current implementation Euclid-MCP uses Prolog.  
Prolog is a 50-year-old battle-tested logic engine. Using it as a "deduction coprocessor" lets small LLMs perform complex multi-step reasoning without needing larger, more expensive models. The intermediate language strips away Prolog's syntax quirks while keeping its logical core.

A specific [benchmark](benchmarks/docs/02-rbac-at-scale.md) demonstrate the difference: with 1 000+ facts, LLMs alone score 2/5 while Euclid-MCP scores 5/5 — and runs 7× faster while outputting 14× fewer tokens.


## Tools

Euclid-MCP exposes **8 tools**, each with a specific purpose:

| Tool | Purpose |
|------|---------|
| `reason` | Main deduction — get solutions + proof trees |
| `explain` | Readable, natural-language reasoning steps |
| `diagnose` | Understand why a query succeeds or fails |
| `what_if` | Test modifications before applying them |
| `check_kb` | Validate KB consistency before reasoning |
| `register_kb` | Register a named KB under a `kb_id` |
| `unregister_kb` | Remove a named KB from the registry |
| `list_kbs` | List registered named KBs (metadata) |

### `reason`

Main tool for verifiable deterministic reasoning.

| Parameter | Type | Default | Description |
|-----------|------|---------|-------------|
| `knowledge` | `string?` | — | Facts & rules in text or YAML format |
| `kb_id` | `string?` | — | Reference a KB registered via `register_kb` |
| `delta_knowledge` | `string?` | — | Session-specific facts appended to the `kb_id` base |
| `query` | `string?` | — | Override query (optional) |
| `max_solutions` | `int` | `5` | Max solutions to return |
| `max_depth` | `int` | `30` | Max proof tree depth |

**Returns** `ReasonResult` with `solutions[]` — each containing variable bindings and a proof tree.

### `explain`

Deterministic proof-tree → natural-language reasoning steps. No LLM involved: it
walks the proof tree of each solution and renders every step in plain language,
citing the rule ID (`# RULE: <id>`) when a rule has one. Use it to turn a proof
into an auditable, human-readable explanation.

| Parameter | Type | Default | Description |
|-----------|------|---------|-------------|
| `knowledge` | `string?` | — | Facts & rules in text or YAML format |
| `kb_id` | `string?` | — | Reference a KB registered via `register_kb` |
| `delta_knowledge` | `string?` | — | Session-specific facts appended to the `kb_id` base |
| `query` | `string?` | — | Override query (optional) |
| `max_solutions` | `int` | `5` | Max solutions to return |
| `max_depth` | `int` | `30` | Max proof tree depth |

**Returns** `ExplanationResult` with `explanations[]` — each containing variable
bindings, an ordered list of natural-language `steps`, and language-independent
`structured_steps` (typed `kind`/`goal`/`rule_id`/`body`, ready for localized
rendering in a UI).

### `diagnose`

Query analysis — understand why a query succeeds or fails.

| Parameter | Type | Default | Description |
|-----------|------|---------|-------------|
| `knowledge` | `string?` | — | Facts & rules in text or YAML format |
| `kb_id` | `string?` | — | Reference a KB registered via `register_kb` |
| `delta_knowledge` | `string?` | — | Session-specific facts appended to the `kb_id` base |
| `query` | `string` | — | Query to diagnose |
| `mode` | `string` | `why` | One of: `why`, `why_not`, `what_needs` |
| `max_solutions` | `int` | `5` | Max solutions to return |
| `max_depth` | `int` | `30` | Max proof tree depth |

**Modes:**
- `why` — explain why a query holds (or that it doesn't)
- `why_not` — explain why a query fails (missing facts/rules)
- `what_needs` — suggest what would make a false query true

**Returns** `DiagnosisResult` with `holds`, `findings[]`, `conclusion`, and optionally `proof`.

### `what_if`