Euclid-MCP: an MCP server for deterministic logical reasoning via Prolog

Source: arXiv — 2026-07-23

Summary

Euclid-MCP is an open-source MCP server, built by Bartolomeo Bogliolo, that gives LLM agents access to a deterministic SWI-Prolog reasoning engine instead of asking the model to do exact logical inference itself. The bridge between agent and engine is Euclid-IR, a new engine-agnostic intermediate representation for Horn-clause logic designed to be easy for LLMs to generate and easy for humans to audit. The server exposes a compact tool interface built around a translate-run-inspect-repair loop, so the agent gets back proof traces and derivation logs rather than an opaque yes/no answer. The paper frames this as a fix for a specific mismatch: RAG-style semantic retrieval is a poor fit for rule-centric decisions that must follow logically from explicit policies, not from textual similarity.

Key Takeaways

• Core architecture is a hybrid split: a lightweight LLM describes the world as facts and rules in Euclid-IR, while a separate deterministic Prolog engine performs the actual deduction — the model no longer has to "be" the reasoner.
• Euclid-IR is pitched as engine-agnostic: it's a Horn-clause representation meant to compile to Prolog today but potentially to other backends later, decoupling the LLM-facing format from the execution engine.
• The tool interface follows a translate-run-inspect-repair loop, meaning failed or incomplete derivations can be inspected and the agent can iteratively patch its own logic program rather than getting a single opaque failure.
• Full proof traces and derivation logs are returned to the calling agent, giving verifiability that a plain LLM answer or a black-box tool call wouldn't provide.
• Positioned against RAG for a specific failure mode: semantic-similarity retrieval doesn't guarantee that a conclusion actually follows from stated rules/policies, which is exactly the gap symbolic deduction closes.

Reel Script

Hook

LLMs are great at sounding logical and bad at actually being logical. Ask one to chain five rules together — an eligibility policy, a tax rule, a compliance check — and it'll give you a confident answer that's wrong just often enough to be dangerous in production.

Core Concept

Here's the underlying idea: don't fix the LLM, route around it. Prolog is a decades-old logic programming language built for exactly one job — given a set of facts and if-then rules, deduce what's true, with zero guessing. It's deterministic: same input, same output, every time, with a receipt showing exactly how it got there. MCP, Model Context Protocol, is just the plumbing — it's how an LLM agent calls out to an external tool and gets a structured result back, the same way it might call a calculator or a database. Euclid-MCP wires those two together. The LLM keeps doing what LLMs are actually good at — reading messy text, extracting facts and rules, describing the world in plain language — and then hands the actual deduction off to Prolog running underneath. Think of the LLM as a paralegal summarizing a contract into clean bullet points, and Prolog as the judge who applies those bullet points with zero room for improvisation.

Hands-On

The pipeline has three hops, and it's genuinely diagrammable. Hop one: the LLM agent takes a task — say, "does this applicant qualify under these five policy rules" — and translates it into Euclid-IR, a Horn-clause format designed specifically to be easy for an LLM to write and easy for a human to read on a diff. Hop two: Euclid-IR compiles down into actual Prolog and runs against the SWI-Prolog engine, which performs pure symbolic deduction — no sampling, no hallucination surface. Hop three: instead of just returning true or false, the engine sends back a full derivation log — the exact chain of rule applications that produced the answer. And critically, this isn't a one-shot pipe. It's a loop: translate, run, inspect, repair. If the Prolog program is incomplete or throws an error, the agent inspects the trace, patches its own Euclid-IR, and reruns — the same way you'd iterate on a failing unit test, except the test is "does this conclusion actually follow from the rules." That inspect-repair step is what turns this from a novelty demo into something you could actually trust in a policy-heavy or compliance-heavy pipeline.

Takeaway

If your agent's job involves following explicit rules — eligibility, compliance, policy logic — semantic similarity was never going to cut it, and Euclid-MCP is a solid, verifiable pattern for offloading that to a real reasoner. Worth a look if you're building anything where "the model felt confident" isn't good enough.

Discussion

(No questions yet — ask follow-ups via a Claude Code chat session on this repo; answers get appended here.)