Euclid-MCP

Euclid-MCP

用于逻辑推理的 MCP 服务——将事实转化为形式化证明。

Euclid-MCP 是一种混合认知架构：轻量级大模型用事实描述世界，确定性引擎负责实际推演。大模型无需推理，只需进行描述。

借助 Euclid-MCP，8B 模型可以解决连 400B+ 云端模型都难以应对的推理任务，因为引擎会以确定性方式处理推演。每个答案都附带证明树，因此你可以追溯结论成立的原因，而不仅仅是结论是什么。你可以用它执行 RBAC 策略、审计云合规性、验证贷款资格规则，或推理任何要求答案可解释且可验证的领域。

Euclid-MCP 使用 Python 编写，并采用 Euclid-IR：一种面向 AI Agent 和人类设计的易读中间语言。它使用 SWI-Prolog 作为主要推理引擎；如果无法使用 SWI-Prolog（例如在精简容器中），则使用纯 Python 编写的 native engine，直接解释 Euclid-IR（参见 docs/NATIVE_ENGINE.md）。 它支持多种使用方式：AI Agent（OpenCode、Claude、Cursor）可通过 MCP 使用；工具和自动化平台（n8n、Zapier、Make）可通过 HTTP 使用；也可通过 Python API 直接集成。Euclid-IR 规则还可用于为 RAG 流水线提供增强，实现确定性的策略执行。

工作原理

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

1. 使用简单的中间语言接收事实、规则和查询
2. 转换为 Prolog，并使用元解释器捕获证明树
3. 通过持久运行的 SWI-Prolog 引擎进程执行（使用 stdin/stdout 上的 JSON 行协议；每次调用都会重新加载工作区，无需承担启动进程的开销）
4. 将解答和证明树作为结构化 JSON 返回

其他工具（explain、diagnose、what_if、check_kb）在此核心流程基础上提供自然语言解释、分析、场景测试和验证功能。

大模型负责描述。Euclid MCP 负责证明。

知识库

对于较小的知识库，可以在每次请求中提供事实和规则。

知识库可以在服务启动时加载，并在后续调用中重复使用，因此 Agent 只需传递当前查询所需的会话专属事实。 这可以最大限度地减少 token 使用量、提升性能，还能让小型大模型基于大型规则集进行推理，而无需在每次请求时重建整个知识库。

中间语言

尽管 Euclid-MCP 当前使用 Prolog 引擎，但无需使用 Prolog 语法。
Euclid-IR（中间表示）是一种用于逻辑推理的声明式中间表示。 变量使用 $name，蕴含使用 IF，合取使用 AND。

文本格式：

human(socrates)
mortal($x) IF human($x)

? mortal($who)

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)

完整语言参考：docs/EUCLID_IR.md

Euclid-IR 语法参考

元素	语法	示例
事实	predicate(args)	parent(tom, bob)
变量	$name（小写）	$who、$x、$count
蕴含	IF	mortal($x) IF human($x)
合取	AND	p($x) AND q($x)
析取	OR	can($u) IF is_admin($u) OR has_role($u, auditor)
分组	(...)	(is_admin($u) OR support($u)) AND active($u)
否定	NOT	NOT active($user)
布尔字面量	规则体中的 true / false	merchant($m) IF false
查询	? predicate	? ancestor(tom, $who)
字符串字面量	"..." 或 '...'	"[email protected]"
多行规则	规则体位于下一行	rule($x) IF\n body($x)

算术比较

规则支持在推导过程中求值的算术比较：

# 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

支持的运算符： >、>=、<、<=、==、is、!=

多行规则

规则可以跨多行编写，以提高可读性：

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)

查询中的合取

查询可以组合多个谓词：

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

当两个条件同时满足时，此查询会返回相应的解。

析取（OR）

规则体可以使用 OR 表示多个备选项。解析器会在加载时将每个备选项展开为独立的 Horn 子句，因此求解器始终只处理纯 Horn 子句：

# A user can deploy when they are an admin, OR a dev on an approved env
can_deploy($u, $env) IF
    is_admin($u) OR
    (has_role($u, dev) AND env_approved($u, $env))

AND 的优先级高于 OR；带括号的分组会以分配方式展开。 NOT 仅作用于单个目标。每个展开分支都会保留 # RULE: <id>，因此可以根据源规则审计证明。

为什么使用外部推理？

外部推理有多项优势：

• 确定性
• 可解释
• 可验证
• 成本低
• 后端可替换

当前实现中，Euclid-MCP 使用 Prolog。
Prolog 是一款历经 50 年实战检验的逻辑引擎。将它用作“推导协处理器”，小型大模型便能执行复杂的多步推理，而无需使用更大、成本更高的模型。中间语言去除了 Prolog 的语法细节，同时保留其逻辑核心。

一项特定的基准测试展示了这种差异：在 1 000+ 个事实的情况下，大模型单独运行得分为 2/5，而 Euclid-MCP 得分为 5/5；同时速度快 7 倍，输出的 token 少 14 倍。

工具

Euclid-MCP 提供 8 个工具，各有特定用途：

工具	用途
reason	主要推导工具——获取解和证明树
explain	以自然语言呈现的推理步骤
diagnose	了解查询成功或失败的原因
what_if	在应用修改前测试修改效果
check_kb	推理前验证 KB 的一致性
register_kb	在 kb_id 下注册一个命名 KB
unregister_kb	从注册表中移除一个命名 KB
list_kbs	列出已注册命名 KB 的元数据

reason

用于可验证、确定性推理的主要工具。

参数	类型	默认值	描述
knowledge	string?	—	文本或 YAML 格式的事实和规则
kb_id	string?	—	引用通过 register_kb 注册的 KB
delta_knowledge	string?	—	会话专属事实，追加到 kb_id 的基础知识中
query	string?	—	覆盖查询（可选）
max_solutions	int	5	返回的最大解数
max_depth	int	30	证明树的最大深度

返回值为 ReasonResult，其中包含 solutions[]；每个解都包含变量绑定和证明树。

explain

将确定性证明树转换为自然语言推理步骤。不涉及大模型：它会遍历每个解的证明树，以通俗语言呈现每一步，并在规则有 ID 时引用规则 ID（# RULE: <id>）。可用于将证明转换为可审计、易于阅读的解释。

参数	类型	默认值	描述
knowledge	string?	—	文本或 YAML 格式的事实和规则
kb_id	string?	—	引用通过 register_kb 注册的知识库
delta_knowledge	string?	—	追加到 kb_id 基础知识库的会话专属事实
query	string?	—	覆盖查询（可选）
max_solutions	int	5	返回的最大解数
max_depth	int	30	最大证明树深度

返回 ExplanationResult，包含 explanations[]。每项都包含变量绑定、有序的自然语言 steps 列表，以及与语言无关的 structured_steps（类型化的 kind/goal/rule_id/body，可用于在 UI 中进行本地化呈现）。

diagnose

查询分析——了解查询为何成功或失败。

参数	类型	默认值	描述
knowledge	string?	—	文本或 YAML 格式的事实和规则
kb_id	string?	—	引用通过 register_kb 注册的知识库
delta_knowledge	string?	—	追加到 kb_id 基础知识库的会话专属事实
query	string	—	要诊断的查询
mode	string	why	可选值：why、why_not、what_needs
max_solutions	int	5	返回的最大解数
max_depth	int	30	最大证明树深度

模式：

• why — 解释查询为何成立（或不成立）
• why_not — 解释查询为何失败（缺少事实或规则）
• what_needs — 建议如何让错误的查询成立

返回 DiagnosisResult，包含 holds、findings[]、conclusion，以及可选的 proof。

what_if

场景分析——对知识库应用修改并比较结果。

参数	类型	默认值	描述
base_knowledge	string?	—	基础事实和规则
kb_id	string?	—	引用通过 register_kb 注册的知识库
delta_knowledge	string?	—	追加到 kb_id 基础知识库的会话专属事实
modifications	string	—	添加 + fact(...)，移除 - fact(...)
query	string	—	要评估的查询
max_solutions	int	5	返回的最大解数
max_depth	int	30	最大证明树深度

返回 WhatIfResult，包含 before_count、after_count、delta、solutions_before、solutions_after、conclusion。

check_kb

知识库验证器——在运行推理前检查一致性。

参数	类型	默认值	描述
knowledge	string?	—	文本或 YAML 格式的事实和规则
kb_id	string?	—	引用通过 register_kb 注册的知识库
delta_knowledge	string?	—	追加到 kb_id 基础知识库的会话专属事实

返回 KBCheckResult，包含 valid、errors[]、warnings[]、facts_count、rules_count、predicates_count 和 predicates[]。其中 predicates[] 是谓词清单（名称 → 元数、事实数、规则数），也可作为大模型提取信息时的约定。

结果中的 KB 标识

每个工具结果——ReasonResult、ExplanationResult、DiagnosisResult、 WhatIfResult 和 KBCheckResult——都包含两个标识字段：

字段	值
content_hash	KB 文本载荷的 sha256（用于推理的确切来源）
version	KB 的 @version 指令；如果不存在，则为 null

这些字段存在于每条返回路径中，包括错误分支，因此结果始终可以追溯到其所依据的确切 KB：任何拥有 .euclid 文本和 Euclid-MCP 的人都可以重新计算哈希并验证。这是基于引擎构建 KB 版本管理、签名和审计跟踪的基础。

{
  "query": "mortal($who)",
  "solutions": [...],
  "elapsed_ms": 12.4,
  "content_hash": "a3f9c1e4b82d55f0…",
  "version": "1.0"
}

KB 预加载

知识库可以在服务器启动时加载一次，并在多次调用间重复使用，这样 Agent 只需传入当前查询特有的会话事实。

可通过 EUCLID_KB_PATH 环境变量或 --kb-path CLI 标志，按文件路径预加载 KB：

# Environment variable
EUCLID_KB_PATH=/path/to/policies.euclid python3 -m euclid_mcp

# CLI flag (MCP stdio, console script, and HTTP API)
python3 -m euclid_mcp --kb-path /path/to/policies.euclid
python3 integrations/euclid_api.py --kb-path /path/to/policies.euclid --port 8080

行为：

• 文件会在启动时通过 check_kb 验证；如果文件缺失、无法读取、超出大小限制或无效，服务器会立即失败并给出明确消息。
• reason、explain、diagnose、what_if 和 check_kb 上的 knowledge/base_knowledge 变为可选：显式传入的值始终优先；传入空值时会回退到预加载的 KB。如果两者都没有，工具会返回明确的“No knowledge provided”错误。
• 预加载 KB 的 Markdown 摘要（事实、规则和谓词的数量，谓词清单，以及包含 ID 的规则）会附加到服务器指令中，因此 Agent 无需额外调用工具即可了解 KB 覆盖的内容。

向后兼容：显式传入 knowledge 的行为与之前完全相同。

命名 KB（kb_id + delta_knowledge）

KB 也可以通过 kb_id 注册一次，之后每次调用都可以引用它，而无需重新发送文本——内存中的注册表按服务器实例隔离，因此各副本会在启动时重新注册自己的 KB（与 HTTP API 的横向扩展模型一致）。每个实例最多支持 32 个 KB；register_kb 会覆盖已有的 kb_id（用于幂等更新）。

# Register once — validated with check_kb first
register_kb(kb_id="rbac-policy", knowledge="has_role(alice, admin) ...\n? $role ...")

# Reference it on every call
result = reason(kb_id="rbac-policy", query="can_deploy($user, prod)")

# Session-specific facts on top of the registered base (no re-registration):
result = reason(
    kb_id="rbac-policy",
    delta_knowledge="has_role(alice, dev)\nhas_env(dev, staging)",
    query="can_deploy($user, staging)",
)

• register_kb(kb_id, knowledge) — 验证 kb_id（允许列表为 [a-z0-9_-]{1,64}）和 KB（check_kb），然后存储。返回记录：registered、kb_id、content_hash、version、facts、rules、predicates。未知 ID 会被拒绝；注册表已满时会返回错误。
• unregister_kb(kb_id) — 移除 KB；返回 removed: true/false。
• list_kbs() — 列出已注册的 KB（仅元数据，不含源文本）。

在 reason、explain、diagnose、what_if、check_kb 上的解析优先级为：显式传入的 knowledge/base_knowledge 优先 → 否则使用 kb_id（未知 ID → Unknown kb_id: <id>；delta_knowledge 会与已注册的源文本拼接）→ 否则使用 EUCLID_KB_PATH 预加载内容 → 否则返回明确的“No knowledge provided”错误。不带 kb_id 使用 delta_knowledge 会报错。kb_id 结果中的 content_hash/version 根据生效后的源文本（基础内容 + 增量内容）计算，因此结果始终可以追溯到实际用于推理的确切文本。

HTTP API 通过 POST /register-kb、POST /unregister-kb 和 POST /list-kbs 提供相同的流程。

安装

pip

# Prerequisite: Python ≥ 3.10

# SWI-Prolog (for better performances)
brew install swi-prolog

# Install
pip install euclid-mcp

从源码安装

git clone https://github.com/Euclid-BG/Euclid-MCP
cd Euclid-MCP
python3 -m venv .venv && source .venv/bin/activate
pip install -e .

Docker

无需在本地安装 SWI-Prolog——镜像已包含所有内容。

# Build
docker build -t euclid-mcp .

# MCP stdio mode (for local MCP clients)
docker compose run --rm euclid-mcp

# HTTP API mode (for n8n, Zapier, remote access)
docker compose up euclid-api
# API available at http://localhost:8080

完整详情请参阅集成中的 Docker。

使用

通过 MCP（OpenCode、Claude 等）

{
  "mcpServers": {
    "euclid-mcp": {
      "command": "python3",
      "args": ["-m", "euclid_mcp"],
      "cwd": "/path/to/euclid-mcp"
    }
  }
}

通过 Python

from euclid_mcp.server import reason, explain, diagnose, what_if, check_kb

# Reasoning
result = reason(knowledge="""
    human(socrates)
    mortal($x) IF human($x)
    ? mortal($who)
""")
for sol in result.solutions:
    print(sol.substitutions, sol.proof.type)

# Explanation — readable reasoning steps (cites rule IDs when present)
expl = explain(
    knowledge="human(socrates)\nmortal($x) IF human($x)  # RULE: BIO-001",
    query="mortal($who)"
)
for e in expl.explanations:
    print(e.substitutions, e.steps)
    print(e.structured_steps)  # typed, language-independent steps

# Diagnosis — why does a query fail?
diag = diagnose(
    knowledge="human(socrates)\nmortal($x) IF human($x)",
    query="mortal(plato)",
    mode="why_not"
)
print(diag.conclusion)

# What-if — how does adding a fact change results?
scenario = what_if(
    base_knowledge="human(socrates)\nmortal($x) IF human($x)",
    modifications="+ human(plato)",
    query="mortal($who)"
)
print(f"Before: {scenario.before_count}, After: {scenario.after_count}")

# KB validation
check = check_kb(knowledge="human(socrates)\nmortal($x) IF human($x)")
print(f"Valid: {check.valid}, Errors: {check.errors}")

通过 CLI

euclid-cli 命令可在终端中调用五种推理工具（reason、explain、 diagnose、what_if、check_kb）。它从 .euclid 文件（-f）或内联内容（--knowledge）中读取 KB；如果两者都没有，则使用 EUCLID_KB_PATH/预加载内容，并通过 --backend （auto | prolog | native）选择后端。查询来自 --query，或来自 KB 文件中的 ? 行。

不带子命令运行即可打开交互式 Euclid-IR REPL — 直接输入事实、规则和 ? query 行， 就像使用 swipl 或 psql 一样。会话知识库会在各次查询间累积。

$ euclid-cli
Euclid-MCP REPL — type facts and rules in Euclid-IR, then `? query`.
Commands: :help  :check  :kb  :load  :explain  :diagnose  :what-if  :reset  :quit

euclid > human(socrates)
euclid > mortal($x) IF human($x)
euclid > ? mortal($who)
Query: mortal($who)
Solution 1:
  who: socrates
mortal(socrates)  [rule]
  human(socrates)  [fact]

euclid > :what-if + human(plato)
Solutions: 1 -> 2 (delta: more)
euclid > :quit

REPL 元命令：:check、:kb、:load <file>、:explain [query]、 :diagnose <query> [why|why_not|what_needs]、:what-if <mods>、:reset、 :quit。多行规则在 IF/AND 后继续输入（提示符变为 ... >）。 通过管道传入的输入会以批处理脚本的方式运行相同循环，不显示提示符：

printf 'human(socrates)\nmortal($x) IF human($x)\n? mortal($who)\n' | euclid-cli

# Validate a knowledge base
euclid-cli check -f policies.euclid

# Run a deduction (query taken from the ? line in the file)
euclid-cli reason -f policies.euclid

# Explicit query + limits
euclid-cli reason -f policies.euclid --query "can_deploy($user, prod)" \
    --max-solutions 10 --max-depth 40

# Inline KB (no file)
euclid-cli reason --knowledge "human(socrates)
mortal(\$x) IF human(\$x)
? mortal(\$who)"

# Readable reasoning steps
euclid-cli explain -f policies.euclid

# Why does a query fail?
euclid-cli diagnose -f policies.euclid --query "can_deploy(bob, prod)" \
    --mode why_not

# What-if: how does adding a fact change the answer?
euclid-cli what-if -f policies.euclid \
    --modifications "+ has_role(bob, deployer)" --query "can_deploy(bob, prod)"

# Force the pure-Python native engine (no SWI-Prolog)
euclid-cli --backend native reason -f policies.euclid

# Machine-readable output
euclid-cli reason -f policies.euclid --json

退出代码：成功时为 0；工具报告错误时为 1（包括 check 检测到无效 KB）；用法错误时为 2。

完整 CLI 参考（所有标志、后端、JSON 输出）：docs/CLI.md

输出示例

{
  "query": "ancestor(tom, $who)",
  "solutions": [
    {
      "substitutions": {"who": "bob"},
      "proof": {
        "type": "rule",
        "goal": "ancestor(tom, bob)",
        "body": "parent(tom, bob)",
        "rule_id": "GEN-1",
        "subproof": {"type": "fact", "goal": "parent(tom, bob)"}
      }
    },
    {
      "substitutions": {"who": "ann"},
      "proof": {
        "type": "rule",
        "goal": "ancestor(tom, ann)",
        "body": "parent(tom, bob), ancestor(bob, ann)",
        "rule_id": "GEN-2",
        "subproof": {
          "type": "and",
          "left": {"type": "fact", "goal": "parent(tom, bob)"},
          "right": {
            "type": "rule",
            "goal": "ancestor(bob, ann)",
            "body": "parent(bob, ann)",
            "rule_id": "GEN-1",
            "subproof": {"type": "fact", "goal": "parent(bob, ann)"}
          }
        }
      }
    }
  ]
}

规则可以通过末尾的 # RULE: <id> 注释携带审计跟踪 ID；该 ID 会显示为证明树中 rule 节点的 rule_id，因此可以引用某个决策（“此结论来自规则 GEN-2”）。

Diagnose 输出

{
  "query": "mortal(plato)",
  "mode": "why_not",
  "holds": false,
  "findings": [
    {
      "type": "satisfied",
      "predicate": "human",
      "detail": "Facts exist for 'human' (1 facts)"
    }
  ],
  "conclusion": "The query fails. Check rule conditions."
}

What-if 输出

{
  "query": "mortal($who)",
  "modifications": "+ human(plato)",
  "before_count": 1,
  "after_count": 2,
  "delta": "more",
  "solutions_before": [{"substitutions": {"who": "socrates"}}],
  "solutions_after": [
    {"substitutions": {"who": "plato"}},
    {"substitutions": {"who": "socrates"}}
  ],
  "conclusion": "Solutions increased: 1 -> 2."
}

Explain 输出

{
  "query": "mortal($who)",
  "explanations": [
    {
      "substitutions": {"who": "socrates"},
      "steps": [
        "mortal(socrates) is derived by rule BIO-001 from: human(socrates).",
        "human(socrates) is asserted as a fact in the knowledge base."
      ]
    }
  ]
}

使用场景

• 小型大模型推理：将大模型（3-8B）的演绎任务交给确定性引擎
• 可解释的决策：每个答案都附带证明树，可用于解释、推理追踪和论证
• 业务规则：验证逻辑链（权限、工作流、合规性）
• 依赖分析：检测循环依赖、进行拓扑排序
• 教育：通过可见的证明链进行交互式逻辑辅导（参见 docs/DIDACTIC.md，这是一份围绕 euclid-cli REPL 编写的分步教学指南）
• 知识预加载：复杂业务规则可以载入 Euclid，而不必使用向量数据库
• 查询诊断：了解查询失败的原因，以及缺少哪些事实/规则
• 场景分析：在将修改应用于生产环境之前，先测试“假设”情景
• KB 验证：在推理前检查知识库是否一致

实际示例

这里提供了多个示例，包括：家谱、RBAC、分类、贷款资格、Cluedo 侦探、IT 安全与合规、LLM 与 Euclid-MCP 对比，…… 最值得关注的是 IT 安全与合规（包含 CIS、AWS、IAM 标准实施、公司政策实施以及数百条数据事实） 和并排对比的 LLM 与 Euclid-MCP。

示例完整说明：docs/EXAMPLES.md

集成

OpenCode

Euclid-MCP 在 .opencode.json 中包含一个预配置的 Agent：

{
  "mcpServers": {
    "euclid-mcp": {
      "command": "python3",
      "args": ["-m", "euclid_mcp"],
      "cwd": "."
    }
  },
  "agents": {
    "reasoning-engine": {
      "description": "Deterministic logic engine",
      "instructions": "Write facts in Euclid IR, use the reason tool...",
      "mcpServers": ["euclid-mcp"]
    }
  }
}

n8n / Zapier / Make

运行 HTTP API：

python3 integrations/euclid_api.py --port 8080

端点	方法	用途
/reason	POST	使用证明树进行演绎
/explain	POST	自然语言推理步骤
/diagnose	POST	查询失败分析
/what-if	POST	场景测试
/check-kb	POST	KB 验证
/register-kb	POST	注册命名 KB（kb_id）
/unregister-kb	POST	移除命名 KB
/list-kbs	POST	列出已注册的命名 KB
/health	GET	健康检查（深度检查会 ping 引擎；仅在引擎卡死时返回 503）
/metrics	GET	Prometheus 指标（开放、只读，绝不包含 KB 内容）

# Reasoning
curl -X POST http://localhost:8080/reason \
  -H "Content-Type: application/json" \
  -d '{"knowledge": "human(socrates)\nmortal($x) IF human($x)\n? mortal($who)"}'

# Explanation
curl -X POST http://localhost:8080/explain \
  -H "Content-Type: application/json" \
  -d '{"knowledge": "human(socrates)\nmortal($x) IF human($x)\n? mortal($who)"}'

# Diagnosis
curl -X POST http://localhost:8080/diagnose \
  -H "Content-Type: application/json" \
  -d '{"knowledge": "human(socrates)\nmortal($x) IF human($x)", "query": "mortal(plato)", "mode": "why_not"}'

# What-if
curl -X POST http://localhost:8080/what-if \
  -H "Content-Type: application/json" \
  -d '{"base_knowledge": "human(socrates)\nmortal($x) IF human($x)", "modifications": "+ human(plato)", "query": "mortal($who)"}'

# KB validation
curl -X POST http://localhost:8080/check-kb \
  -H "Content-Type: application/json" \
  -d '{"knowledge": "human(socrates)\nmortal($x) IF human($x)"}'

# Register a named KB once, then reference it by kb_id
curl -X POST http://localhost:8080/register-kb \
  -H "Content-Type: application/json" \
  -d '{"kb_id": "rbac", "knowledge": "human(socrates)\nmortal($x) IF human($x)"}'

curl -X POST http://localhost:8080/reason \
  -H "Content-Type: application/json" \
  -d '{"kb_id": "rbac", "delta_knowledge": "human(plato)", "query": "mortal($who)"}'

curl -X POST http://localhost:8080/list-kbs \
  -H "Content-Type: application/json" \
  -d '{}'

curl -X POST http://localhost:8080/unregister-kb \
  -H "Content-Type: application/json" \
  -d '{"kb_id": "rbac"}'

Docker

Docker 镜像捆绑了 SWI-Prolog + Python，因此无需本地安装前置依赖。 基础镜像：swipl:stable（Debian Bookworm）。

通过 docker-compose 使用两种模式：

# MCP stdio — pipe to a local MCP client
docker compose run --rm euclid-mcp

# HTTP API — expose REST endpoints on port 8080
docker compose up euclid-api

独立使用：

# Build
docker build -t euclid-mcp .

# Run HTTP API
docker run --rm -p 8080:8080 euclid-mcp \
  python3 integrations/euclid_api.py --port 8080

# Run MCP stdio (interactive)
docker run --rm -i euclid-mcp

# Quick test — reason directly from CLI
docker run --rm euclid-mcp python3 -c "
from euclid_mcp.server import reason
r = reason(knowledge='human(socrates)\nmortal(\$x) IF human(\$x)\n? mortal(\$who)')
print(r.solutions[0].substitutions)
"

**Docker 镜像大小：**约 370 MB（SWI-Prolog + Python 3.11 + 依赖项）。

**仅原生模式（精简版）：**较小的镜像，使用纯 Python Euclid-IR 引擎， 不包含 SWI-Prolog（EUCLID_BACKEND=native）。适合空间有限的容器， 也适合作为小型知识库的默认选项。

# Build
docker build -f Dockerfile.native -t euclid-mcp-native .

# Run MCP stdio (interactive)
docker compose run --rm euclid-mcp-native

# Run HTTP API
docker run --rm -p 8080:8080 euclid-mcp-native \
  python3 integrations/euclid_api.py --port 8080

# Quick test — reason directly from CLI
docker run --rm euclid-mcp-native python3 -c "
from euclid_mcp.server import reason
r = reason(knowledge='human(socrates)\nmortal(\$x) IF human(\$x)\n? mortal(\$who)')
print(r.solutions[0].substitutions)
"

基础镜像：python:3.12-slim。

CLI 流水线

echo '{"knowledge": "red(apple)\\n? red($x)"}' | python3 integrations/euclid_cli.py

完整详情请参阅 integrations/README.md。

可扩展性

Euclid-MCP 引擎具有持久性：每个服务实例运行一个长期存活的 SWI-Prolog 进程，通过 JSON 行管道按请求重新加载，而不是每次调用都启动 Prolog。 单个实例一次处理一个请求。 请求保持无状态： 每个请求都携带自己的知识库（或使用预加载的知识库）， 因此实例之间互不共享。

这使 Euclid-MCP 可以水平扩展：

• HTTP API — 在负载均衡器（nginx、Kubernetes Service 等）后运行任意数量的实例。无需会话亲和性：任何实例都可以处理任何请求。
• MCP stdio — 按设计，每个 MCP 客户端都会启动自己的实例，从而在客户端之间实现自然隔离和并行处理。
• 资源占用 — 每个实例运行一个 swipl 进程（约几十 MB），而不是每个请求启动一个短暂运行的进程，因此单个实例即可低成本处理大量请求。

生产环境参考架构——为 HAProxy 后的副本集群配置负载均衡、资源限制、安全加固和监控： docs/PRODUCTION.md。

开发

要求：Python ≥ 3.10、SWI-Prolog。

# Install in editable mode with dev dependencies
python3 -m venv .venv && source .venv/bin/activate
pip install -e ".[dev]"

# Lint
ruff check .

# Type check
mypy euclid_mcp integrations

# Tests with coverage
pytest --cov=euclid_mcp --cov=integrations

CI 工作流（.github/workflows/ci.yml）会在推送和拉取请求时，针对 Python 3.10–3.14 执行相同的检查。

日志与追踪

每次工具调用都会记录其名称、耗时和结果。设置 EUCLID_LOG_LEVEL（取值为 DEBUG、INFO、 WARNING、ERROR、CRITICAL）即可启用结构化日志，例如 EUCLID_LOG_LEVEL=INFO。未设置该变量时，仅输出警告和错误。

HTTP API 也支持请求追踪：发送 X-Request-Id 标头，该标头会在响应中原样返回，并包含在访问日志中。

监控与指标

HTTP API 在 GET /metrics 上公开 Prometheus 指标（开放、只读，绝不包含知识库内容）：各工具调用/错误计数器和延迟直方图、引擎请求/重启/超时、HTTP 流量、返回的解、身份验证失败次数和进程运行时间——始终启用，无额外依赖 （euclid_mcp/metrics.py）。GET /health 是深度检查，会 ping 引擎并报告其工作区统计信息（仅当引擎卡死时返回 503）。

curl -s localhost:8080/metrics

完整技术栈（包含 Prometheus + Grafana + cAdvisor、仪表板和告警规则）：monitoring/README.md。

什么是 Prolog？

Prolog（源自 PROgrammation en LOGique）是一种声明式逻辑编程 语言：你无需告诉机器如何计算答案，而是陈述事实和规则，让它通过合一和回溯找出由此推导出什么。Prolog 诞生于 20 世纪 70 年代初，至今仍是经受了实战考验的符号推理工具之一。

Euclid-MCP 使用 SWI-Prolog 作为推理 引擎。SWI-Prolog 是成熟的 开源实现，自 1987 年以来持续开发并免费提供，广泛应用于工业界、学术界和研究领域。你可以用 Euclid-IR 编写规则；转换器会将其编译为 Prolog，而 SWI-Prolog 则执行推理并生成证明树，让 Euclid-MCP 的每个答案都可验证。

Euclid 是什么？

Euclid 是一位古希腊数学家。他在亚历山大生活和教学，通过严谨的逻辑证明奠定了几何学和数论的基础。

Euclid-MCP 不是：

• 大模型
• 知识库
• 向量数据库
• Agent 框架
• 规划器

Euclid-MCP 是一个确定性推理引擎，可供上述任何一种系统使用。
Euclid-MCP 还能让 Edge 硬件上的小型大模型给出确定且可解释的回复。

许可证

Apache 2.0