
Euclid-MCP
io.github.meob由 GitHub 帳號 meob 發布v0.4.5更新於 Oct 24, 2026
Deterministic logical reasoning engine — facts in Euclid IR, solutions with proof trees
概覽
一個本機 MCP 伺服器,對以 Euclid-IR 撰寫的事實執行確定性邏輯推論,回傳附證明樹的解。
- 可以做什麼
- 對 Euclid-IR 事實與規則執行推論,回傳解與證明樹,並在每個結果附上內容雜湊與版本,以便鎖定所用的知識庫。把證明樹轉成引用規則 ID 的白話推理步驟。診斷查詢成立或失敗的原因,並在套用前測試假設性修改。驗證知識庫一致性並檢視其述詞清單。依 kb_id 註冊、列出與移除具名知識庫,並可為單次呼叫附加增量事實。
- 適用情境
- 適合答案必須可解釋、可驗證而非自由生成的場合:業務規則、存取控制或合規檢查、相依性分析,以及把推論從小模型卸載到確定性引擎。也適合用可見的證明鏈進行邏輯教學。
- 執行需求
- 以本機 stdio 程序執行,可透過 uvx 或 pip 從 PyPI 安裝;需要 Python 3.10 或更新版本。建議安裝 SWI-Prolog 以獲得更好效能,也可退回純 Python 原生引擎;Docker 映像已內建兩者。可透過 EUCLID_KB_PATH 環境變數或 --kb-path 參數預先載入知識庫。未宣告驗證或 API 金鑰。
安裝
在 SourceWeft 中
- 開啟 儀表板中的 Euclid-MCP,將其新增到工作區。
- 為需要使用其工具的對話啟用該服務。
Desktop only,透過 STDIO。 STDIO 服務會啟動本機處理程序,因此需要 SourceWeft 桌面主機。
其他 MCP 客戶端
參照 儲存庫 中的啟動說明。
README
Euclid-MCP
[Euclid-MCP MCP server] [PyPI version] [Python versions] [License] [CI] [Coverage]
MCP server for logical reasoning — turns facts into formal proofs.
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 (see 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
- Receive facts, rules, and a query in a simple intermediate language
- Translate into Prolog with a meta-interpreter for proof tree capture
- Execute via a persistent SWI-Prolog engine process (JSON-lines protocol on stdin/stdout; the workspace is reloaded per call, no process spawn overhead)
- 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:
YAML format:
Full language reference: docs/EUCLID_IR.md
Euclid-IR Syntax Reference
Arithmetic Comparisons
Rules support arithmetic comparisons that are evaluated during deduction:
Supported operators: >, >=, <, <=, ==, is, !=
Multi-line Rules
Rules can span multiple lines for readability:
Conjunctions in Queries
Queries can combine multiple predicates:
This returns solutions where both conditions are satisfied simultaneously.
Disjunction (OR)
Rule bodies can express alternatives with OR. The parser expands each
alternative into its own Horn clause at load time — the solver only ever
sees pure Horn clauses:
AND binds tighter than OR; parenthesized groups expand distributively.
NOT applies to single goals only. A # RULE: <id> is carried by every
expanded branch, so proofs stay auditable against the source rule.
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 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:
reason
Main tool for verifiable deterministic reasoning.
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.
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.
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
Scenario analysis — apply modifications to a knowledge base and compare results.
Returns WhatIfResult with before_count, after_count, delta, solutions_before, solutions_after, conclusion.
check_kb
Knowledge base validator — check for consistency before running deduction.
Returns KBCheckResult with valid, errors[], warnings[], facts_count, rules_count, predicates_count, and predicates[] — the predicate inventory (name → arities, facts, rules counts) that doubles as the contract for LLM extraction.
KB identity in results
Every tool result — ReasonResult, ExplanationResult, DiagnosisResult,
WhatIfResult, and KBCheckResult — carries two identity fields:
The fields are present on every return path, including error branches, so a
result can always be pinned to the exact KB it was computed from: anyone with
the .euclid text and Euclid-MCP can recompute the hash and verify it. This is
the foundation for KB versioning, signatures, and audit trails built on top of
the engine.
KB Preload
A knowledge base can be loaded once at server startup and reused across calls, so agents only pass the session-specific facts for the current query.
Preload a KB by file path, via the EUCLID_KB_PATH environment variable or a
--kb-path CLI flag:
Behavior:
- The file is validated with
check_kbat startup and the server fails fast with a clear message if the file is missing, unreadable, oversized, or invalid. knowledge/base_knowledgeonreason,explain,diagnose,what_if, andcheck_kbbecome optional: an explicit value always wins, an empty value falls back to the preloaded KB. With neither, tools return a clear "No knowledge provided" error.- A markdown digest of the preloaded KB (fact/rule/predicate counts, predicate inventory, rules with their IDs) is appended to the server instructions, so agents can see what the KB covers without extra tool calls.
Backward compatible: passing knowledge explicitly behaves exactly as before.
Named KBs (kb_id + delta_knowledge)
A KB can also be registered once under a kb_id and then referenced on
every call without resending the text — the in-memory registry is per
server instance, so replicas re-register their KBs on startup (matching the
scale-out model of the HTTP API). Up to 32 KBs per instance; register_kb
overwrites an existing kb_id (update semantics for idempotency).
register_kb(kb_id, knowledge)— validates thekb_id(allowlist[a-z0-9_-]{1,64}) and the KB (check_kb), then stores it. Returns the record:registered,kb_id,content_hash,version,facts,rules,predicates. Unknown ids are rejected; a full registry returns an error.unregister_kb(kb_id)— removes the KB; returnsremoved: true/false.list_kbs()— lists registered KBs (metadata only, no source text).
Resolution precedence on reason, explain, diagnose, what_if,
check_kb: explicit knowledge/base_knowledge wins → else kb_id
(unknown id → Unknown kb_id: <id>; delta_knowledge is concatenated to the
registered source) → else the EUCLID_KB_PATH preload → else a clear
"No knowledge provided" error. delta_knowledge without a kb_id is an
error. content_hash/version on a kb_id result are computed from the
effective source (base + delta), so a result can always be pinned to the
exact text reasoned over.
The HTTP API exposes the same flow as POST /register-kb,
POST /unregister-kb, and POST /list-kbs.
Installation
pip
From source
Docker
No local SWI-Prolog installation needed — the image bundles everything.
See Docker in Integrations for full details.
Usage
Via MCP (OpenCode, Claude, etc.)
Via Python
Via CLI
The euclid-cli command wraps the five reasoning tools (reason, explain,
diagnose, what_if, check_kb) for the terminal. It reads
the KB from a .euclid file (-f), inline (--knowledge), or falls back to
EUCLID_KB_PATH/preload, and selects the backend with --backend
(auto | prolog | native). Queries come from --query or from the ?
lines inside the KB file.
Run with no subcommand to open an interactive Euclid-IR REPL — type
facts, rules and ? query lines directly, like you would in swipl or
psql. The session knowledge base accumulates across queries.
REPL meta-commands: :check, :kb, :load <file>, :explain [query],
:diagnose <query> [why|why_not|what_needs], :what-if <mods>, :reset,
:quit. Multi-line rules continue after IF/AND (prompt becomes ... >).
Piped input runs the same loop as a batch script without prompts:
Exit codes: 0 on success, 1 when the tool reports an error (including an
invalid KB from check), 2 on usage errors.
Full CLI reference (all flags, backends, JSON output): docs/CLI.md
Example output
Rules can carry an audit-trail ID via a trailing # RULE: <id> comment; the ID
is surfaced as rule_id on the rule nodes of the proof tree, so a decision
can be cited ("this derives from rule GEN-2").
Diagnose output
What-if output
Explain output
Use cases
- Small LLM reasoning: Offload deduction from LLMs (3-8B) to a deterministic engine
- Explainable decisions: Every answer comes with a proof tree which allows explanation, reasoning trace, and justification
- Business rules: Validate logic chains (permissions, workflows, compliance)
- Dependency analysis: Circular dependency detection, topological ordering
- Education: Interactive logic tutoring with visible proof chains (see
docs/DIDACTIC.md, a step-by-step teaching guide built around theeuclid-cliREPL) - Knowledge preload: Complex business rules can be loaded in Euclid instead of using a vector database
- Query diagnosis: Understand why queries fail and what facts/rules are missing
- Scenario analysis: Test "what-if" modifications before applying them to production
- KB validation: Check knowledge bases for consistency before reasoning
Real-world examples
There are several examples provided as samples: Genealogy, RBAC, Classification, Loan Eligibility, Cluedo Detective, IT Security & Compliance, LLM vs Euclid-MCP, ... Most interesting ones are the IT Security & Compliance (with CIS, AWS, IAM Standards enforcement, Company Policies implementation, hundreds of Data Facts) and side-by-side LLM vs Euclid-MCP.
Examples full description: docs/EXAMPLES.md
Integrations
OpenCode
Euclid-MCP includes a pre-configured agent in .opencode.json:
n8n / Zapier / Make
Run the HTTP API:
Docker
The Docker image bundles SWI-Prolog + Python, so no local prerequisites are needed.
Base image: swipl:stable (Debian Bookworm).
Two modes via docker-compose:
Standalone usage:
Docker image size: ~370 MB (SWI-Prolog + Python 3.11 + dependencies).
Native-only (slim): a smaller image with the pure-Python Euclid-IR engine
and no SWI-Prolog (EUCLID_BACKEND=native). Best for containers with limited
space or as the default for small knowledge bases.
Base image: python:3.12-slim.
CLI pipeline
See integrations/README.md for full details.
Scalability
Euclid-MCP engine is persistent: a single long-lived SWI-Prolog process per server instance, reloaded per request over a JSON-lines pipe instead of booting Prolog for every call. A single instance handles one request at a time. Requests stay stateless: each one brings its own knowledge base (or uses the preloaded one), so instances share nothing.
This makes Euclid-MCP horizontally scalable:
- HTTP API — run any number of instances behind a load balancer (nginx, a Kubernetes Service, …). No session affinity needed: any instance can serve any request.
- MCP stdio — each MCP client spawns its own instance by design, giving natural isolation and parallelism across clients.
- Resource footprint — one
swiplprocess per instance (~tens of MB) instead of one short-lived process per request, so a single instance serves many requests cheaply.
Reference production architecture — load balancing, resource limits, security
hardening, and monitoring for a replica battery behind HAProxy:
docs/PRODUCTION.md.
Development
Requirements: Python ≥ 3.10, SWI-Prolog.
The CI workflow (.github/workflows/ci.yml) runs these
same checks on push and pull request, across Python 3.10–3.14.
Logging & tracing
Every tool call is logged with its name, elapsed time, and outcome. Enable
structured logs by setting EUCLID_LOG_LEVEL (one of DEBUG, INFO,
WARNING, ERROR, CRITICAL) — e.g. EUCLID_LOG_LEVEL=INFO. Without the
variable, only warnings and errors are emitted.
The HTTP API also supports request tracing: send an X-Request-Id header and
it is echoed back on the response and included in the access logs.
Monitoring & metrics
The HTTP API exposes Prometheus metrics on GET /metrics (open, read-only,
never carries KB content): per-tool call/error counters and latency
histograms, engine requests/restarts/timeouts, HTTP traffic, solutions
returned, auth failures and process uptime — always on, zero dependencies
(euclid_mcp/metrics.py). GET /health is a deep check that pings the
engine and reports its workspace stats (503 only when a wedged engine exists).
For a full stack (Prometheus + Grafana + cAdvisor, dashboard and alert rules
included): monitoring/README.md.
What is Prolog?
Prolog (from PROgrammation en LOGique) is a declarative logic programming language: instead of telling the machine how to compute an answer, you state facts and rules and let it find what follows from them, using unification and backtracking. Born in the early 1970s, it remains one of the most battle-tested tools for symbolic reasoning.
Euclid-MCP uses SWI-Prolog as its inference engine. SWI-Prolog is a mature open-source implementation — continuously developed and freely available since 1987 — widely used in industry, academia, and research. You write your rules in Euclid-IR; the translator compiles them to Prolog, and SWI-Prolog performs the deduction and produces the proof trees that make every Euclid-MCP answer verifiable.
How is Euclid?
Euclid was an ancient Greek mathematician. Living and teaching in Alexandria, he built the foundations of geometry and number theory using rigorous logical proofs.
Euclid-MCP is not:
- an LLM
- a knowledge base
- a vector database
- an agent framework
- a planner
Euclid-MCP is a deterministic inference engine that can be used by any of them.
Euclid-MCP allows deterministic and explainable replies from small LLMs on Edge hardware too.
License
Apache 2.0
來源:README.md,提交 7766a20
工具
0版本歷史
1- v0.4.5最新Sep 16, 2026
評分
已滿足適用檢查項的 50%
該評分衡量此收錄條目的完整程度,依據註冊中心條目、端點與公開來源計算得出。它不是對伺服器本身的評價,也不表示伺服器安全或目前可用:可連通性是帶日期的檢查結果,評分也不包含安裝量或使用者評價。
- 近 30 天內可連通25 分
請保持端點能夠回應 MCP 握手;SourceWeft 每 30 天探測一次。
- 已宣告認證方式10 分
請在註冊中心條目中宣告憑證請求標頭,或保持端點能夠回應探測,以便判定其認證方式。
- 已列出工具15 分
請讓伺服器在無憑證時回應 tools/list,或發布可在沙箱中無憑證啟動的軟體包。
- 描述必需15 分
- 圖示10 分
- 文件15 分
- 授權條款10 分