Euclid-MCP

Euclid-MCP

論理推論のためのMCP サーバー — 事実を形式的な証明に変換します。

Euclid-MCPはハイブリッドな認知アーキテクチャです。軽量なLLMが世界を事実として記述し、決定論的なエンジンが実際の推論を行います。LLMが推論する必要はなく、記述するだけで十分です。

Euclid-MCPを使えば、エンジンが決定論的に推論を処理するため、8Bモデルでも400B超のクラウドモデルさえ行き詰まらせる推論タスクを解決できます。すべての回答には証明木が付属するため、結論が「何であるか」だけでなく、「なぜ成り立つのか」も追跡できます。RBACポリシーの適用、クラウドコンプライアンスの監査、ローン適格性ルールの検証、あるいは説明可能で検証可能な回答が必要なあらゆるドメインでの推論に活用できます。

Euclid-MCPはPythonで記述されており、AIエージェントと人間の両方を対象に設計された、人間が読みやすい中間言語 Euclid-IR を使用します。主要な推論エンジンには SWI-Prolog を使用し、SWI-Prologが利用できない場合（最小構成のコンテナなど）は、Euclid-IRを直接解釈する純粋なPython製の ネイティブエンジン を使用します（docs/NATIVE_ENGINE.mdを参照）。 利用方法は複数あります。AIエージェント（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エンジンプロセスを介して実行します（標準入力／標準出力でのJSON Linesプロトコルを使用し、呼び出しごとにワークスペースを再読み込みするため、プロセス起動のオーバーヘッドはありません）
4. 解と証明木を構造化JSONとして返します

追加のツール（explain、diagnose、what_if、check_kb）は、自然言語による説明、分析、シナリオテスト、検証によって、この基本フローを拡張します。

LLMは記述します。Euclid MCPは証明します。

ナレッジベース

小規模なナレッジベースの場合は、各リクエストに事実とルールを含められます。

ナレッジベースはサーバー起動時に読み込み、呼び出し間で再利用できます。そのため、エージェントは現在のクエリに固有の事実だけを渡せば済みます。 これによりトークン使用量を最小限に抑え、パフォーマンスを向上させ、リクエストごとにナレッジベース全体を再構築することなく、小規模なLLMでも大規模なルールセットを使って推論できるようになります。

中間言語

現在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 を使って選択肢を表現できます。パーサーは読み込み時に各選択肢を個別のホーン節に展開するため、ソルバーが扱うのは純粋なホーン節だけです。

# 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年にわたって実績を積んできたロジックエンジンです。これを「推論コプロセッサ」として使うことで、小規模な LLM でも、より大規模で高価なモデルを必要とせずに、複雑な複数ステップの推論を実行できます。中間言語は、Prolog の構文上の癖を取り除きながら、その論理的な中核を維持します。

特定のベンチマークでは、その違いが示されています。1,000件以上の事実がある場合、LLM 単独では 2/5 のスコアですが、Euclid-MCP は 5/5 を達成します。さらに、実行速度は7倍、出力トークン数は14分の1です。

ツール

Euclid-MCP は、それぞれに特定の目的を持つ8つのツールを公開しています。

ツール	目的
reason	主な推論 — 解と証明木を取得
explain	読みやすい自然言語による推論ステップ
diagnose	クエリが成功または失敗する理由を把握
what_if	変更を適用する前にテスト
check_kb	推論前に KB の整合性を検証
register_kb	名前付き KB を kb_id で登録
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	証明木の最大深度

返り値： solutions[] を含む ReasonResult。各要素には変数の束縛と証明木が含まれます。

explain

決定論的に証明木を自然言語の推論ステップに変換します。LLM は関与しません。各解の証明木をたどり、すべてのステップを平易な言葉で表現します。ルールに ID がある場合は、ルール ID（# RULE: <id>）を示します。証明を監査可能で、人が読みやすい説明に変換するために使用します。

パラメーター	型	デフォルト	説明
knowledge	string?	—	テキストまたは YAML 形式の事実とルール
kb_id	string?	—	register_kb 経由で登録された 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 経由で登録された 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 経由で登録された 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 経由で登録された KB を参照します
delta_knowledge	string?	—	kb_id のベースに追加する、セッション固有の事実

戻り値 KBCheckResult。valid、errors[]、warnings[]、facts_count、rules_count、predicates_count、および predicates[] を含みます。predicates[] は述語の一覧（名前 → アリティ、事実数、ルール数）で、LLM による抽出の契約としても機能します。

結果に含まれる KB の識別情報

すべてのツール結果 — ReasonResult、ExplanationResult、DiagnosisResult、 WhatIfResult、KBCheckResult — には、2 つの識別フィールドが含まれます。

フィールド	値
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 の事前読み込み

ナレッジベースは サーバー起動時に一度だけ 読み込み、複数の呼び出しで再利用できます。これにより、エージェントは現在のクエリに固有の事実だけを渡せばよくなります。

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 付きルール）がサーバーの指示に追加されます。これにより、エージェントは追加のツール呼び出しなしで KB の内容を把握できます。

後方互換性があります。knowledge を明示的に渡した場合の動作は、これまでとまったく同じです。

名前付き KB（kb_id + delta_knowledge）

KB は kb_id を付けて一度登録 し、その後の呼び出しでテキストを再送信せずに参照することもできます。メモリ内レジストリはサーバーインスタンスごとに管理されるため、レプリカは起動時に KB を再登録します（HTTP API のスケールアウトモデルに対応）。1 インスタンスあたり最大 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

詳しくは、Integrations の 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 コマンドは、5 つの推論ツール（reason、explain、 diagnose、what_if、check_kb）をターミナルで使えるようにします。KB は .euclid ファイル（-f）、インライン（--knowledge）から読み込むか、 EUCLID_KB_PATH／事前ロードにフォールバックします。また、バックエンドは --backend（auto | prolog | native）で選択します。クエリは --query または KB ファイル内の ? 行から指定します。

サブコマンドを指定せずに実行すると、対話型の Euclid-IR REPL が起動します。 swipl や psql と同様に、ファクト、ルール、? query 行を直接入力できます。 セッションのナレッジベースは、クエリを実行しても保持されます。

$ 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、ツールがエラーを報告した場合（check による無効な KB を含む）は 1、 使用方法のエラー時は 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 から導かれています」）。

診断の出力

{
  "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."
}

説明の出力

{
  "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."
      ]
    }
  ]
}

ユースケース

• 小規模 LLM の推論：LLM（3～8B）による演繹を、決定論的なエンジンに任せます
• 説明可能な決定：すべての回答に、説明、推論トレース、根拠を示せる証明ツリーが付属します
• ビジネスルール：ロジックチェーン（権限、ワークフロー、コンプライアンス）を検証します
• 依存関係の分析：循環依存の検出、トポロジカルソート
• 教育：証明チェーンを確認できる対話型の論理学習（docs/DIDACTIC.md を参照してください。euclid-cli REPL を使った段階的な学習ガイドです）
• ナレッジの事前ロード：ベクトルデータベースの代わりに、複雑なビジネスルールを Euclid に読み込めます
• クエリの診断：クエリが失敗する理由や、不足しているファクト／ルールを把握できます
• シナリオ分析：本番環境に適用する前に、「what-if」の変更をテストできます
• KB の検証：推論の前に、ナレッジベースの一貫性を確認します

実例

サンプルとして、家系図、RBAC、分類、ローン適格性、Cluedo Detective、IT セキュリティとコンプライアンス、LLM 対 Euclid-MCP など、複数の例が用意されています。 特に興味深いのは、IT セキュリティとコンプライアンス（CIS、AWS、IAM 標準の適用、会社方針の実装、数百件のデータファクトを含む）と、LLM 対 Euclid-MCP の並列比較です。

例の詳細：docs/EXAMPLES.md

統合

OpenCode

Euclid-MCP には、.opencode.json に事前設定済みのエージェントが含まれています。

{
  "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	ヘルスチェック（deep：エンジンに 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 での 2 つのモード：

# 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 プロセスを使用し、呼び出しごとに Prolog を起動するのではなく、JSON Lines パイプを介してリクエストごとに再読み込みします。 1 つのインスタンスが一度に処理するリクエストは 1 つです。 リクエストはステートレスのままです。 それぞれのリクエストが独自のナレッジベースを持ち込む（またはプリロード済みのものを使用する）ため、インスタンス間で共有されるものはありません。

このため、Euclid-MCP は水平スケーリングが可能です。

• HTTP API — ロードバランサー（nginx、Kubernetes Service など）の背後で、任意の数のインスタンスを実行できます。セッションアフィニティは不要です。どのインスタンスでも、どのリクエストにも対応できます。
• MCP stdio — MCP クライアントは設計上、それぞれ独自のインスタンスを起動するため、クライアント間で自然な分離と並列処理が実現します。
• リソース使用量 — リクエストごとに短時間だけ稼働するプロセスを起動する代わりに、インスタンスごとに swipl プロセス 1 つ（数十 MB 程度）を使用するため、1 つのインスタンスで多くのリクエストを低コストで処理できます。

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）では、push とプルリクエストの際に、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 メトリクスを公開します（公開アクセス可能、読み取り専用、KB の内容は含みません）。ツールごとの呼び出し数・エラー数カウンターとレイテンシーヒストグラム、エンジンのリクエスト数・再起動数・タイムアウト数、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 に由来）は宣言型の論理プログラミング言語です。機械に答えの計算方法を指示するのではなく、事実とルールを記述すると、単一化とバックトラッキングを用いて、そこから何が導かれるかを探索します。1970 年代初頭に誕生し、シンボリック推論の分野で今なお最も実績のあるツールの 1 つです。

Euclid-MCP は推論エンジンとして SWI-Prolog を使用します。SWI-Prolog は成熟したオープンソース実装で、1987 年以来継続的に開発され、無料で利用でき、産業界、学術界、研究分野で広く使われています。Euclid-IR でルールを記述すると、トランスレーターがそれを Prolog にコンパイルし、SWI-Prolog が推論を実行して、すべての Euclid-MCP の回答を検証可能にする証明木を生成します。

ユークリッドとは？

ユークリッドは古代ギリシャの数学者です。アレクサンドリアで生活し、教えながら、厳密な論理的証明を用いて幾何学と数論の基礎を築きました。

Euclid-MCPは次のものではありません。

• LLM
• ナレッジベース
• ベクトルデータベース
• エージェントフレームワーク
• プランナー

Euclid-MCPは、これらのいずれからも利用できる決定論的推論エンジンです。
Euclid-MCPを使えば、エッジハードウェア上の小規模なLLMでも、決定論的で説明可能な応答を生成できます。

ライセンス

Apache 2.0