Mcplogic

🚀 MCP Logic

MCP Logicは、TypeScriptで実装された自己完結型の一階論理推論用MCPサーバーです。外部のバイナリ依存関係がなく、様々な論理的なタスクを実行できます。

オリジナルのリポジトリ: https://github.com/angrysky56/mcp-logic/

✨ 主な機能

コア推論

• 定理証明 — 分解法を使用して論理文を証明します。
• モデル探索 — 前提を満たす有限モデルを見つけます。
• 反例検出 — 結論が導けないことを示すモデルを見つけます。
• 構文検証 — 詳細なエラーメッセージを伴って、式を事前に検証します。

エンジン連携

• マルチエンジンアーキテクチャ — 式の構造に基づいて自動的にエンジンを選択します。
• Prologエンジン (Tau-Prolog) — ホーン節、Datalog、等値推論に効率的です。
• SATエンジン (MiniSat) — 一般的な一階論理と非ホーン式を扱います。
• エンジンパラメータ — 明示的なエンジン選択: 'prolog'、'sat'、または 'auto'

高度な論理

• 算術サポート — 組み込み述語: lt、gt、plus、minus、times、divides
• 等値推論 — 反射性、対称性、推移性、合同性の公理を使用します。
• CNFクロージファイケーション — 一階論理を連言標準形に変換します。
• DIMACSエクスポート — 外部のSATソルバー用にCNFをエクスポートします。

MCPプロトコル

• セッションベースの推論 — 知識ベースを段階的に構築します。
• 公理リソース — 参照可能な公理ライブラリ (圏論、ペアノ算術、ZFCなど)
• 推論プロンプト — 背理法による証明、形式化などのテンプレート
• 冗長性制御 — LLMチェーン用のトークン効率の高い応答

インフラストラクチャ

• 自己完結型 — 純粋なnpm依存関係で、外部のバイナリは必要ありません。
• 構造化エラー — 提案付きの機械可読なエラー情報
• 254のテスト — 包括的なテストカバレッジ

🚀 クイックスタート

インストール

git clone <repository>
cd mcplogic
npm install
npm run build

サーバーの起動

npm start

または、自動リロードで開発する場合は:

npm run dev

Claude Desktop / MCPクライアントの設定

MCP設定に以下を追加します:

{
  "mcpServers": {
    "mcp-logic": {
      "command": "node",
      "args": ["/path/to/mcplogic/dist/index.js"]
    }
  }
}

💻 使用例

コア推論ツール

セッション管理ツール

エンジン選択

prove ツールは自動または明示的なエンジン選択をサポートしています:

{
  "name": "prove",
  "arguments": {
    "premises": ["foo | bar", "-foo"],
    "conclusion": "bar",
    "engine": "auto"
  }
}

応答には選択されたエンジンを示す engineUsed が含まれます:

{ "success": true, "result": "proved", "engineUsed": "sat/minisat" }

算術と等値

算術サポート

enable_arithmetic: true で有効にします:

{
  "name": "prove",
  "arguments": {
    "premises": ["lt(1, 2)", "lt(2, 3)", "all x all y all z ((lt(x,y) & lt(y,z)) -> lt(x,z))"],
    "conclusion": "lt(1, 3)",
    "enable_arithmetic": true
  }
}

組み込み述語: lt、gt、le、ge、plus、minus、times、divides、mod

等値推論

enable_equality: true で有効にします:

{
  "name": "prove",
  "arguments": {
    "premises": ["a = b", "P(a)"],
    "conclusion": "P(b)",
    "enable_equality": true
  }
}

反射性、対称性、推移性、合同性の公理が自動的に注入されます。

MCPリソース

MCPリソースプロトコルを介して公理ライブラリを参照できます:

MCPプロンプト

一般的なタスクのための推論テンプレート:

冗長性制御

すべてのツールは verbosity パラメータをサポートしています:

{
  "name": "prove",
  "arguments": {
    "premises": ["man(socrates)", "all x (man(x) -> mortal(x))"],
    "conclusion": "mortal(socrates)",
    "verbosity": "minimal"
  }
}

最小限の応答: { "success": true, "result": "proved" }

式の構文

このサーバーはProver9と互換性のある一階論理 (FOL) 構文を使用しています:

量化子

• all x (...) — 全称量化子 (∀x)
• exists x (...) — 存在量化子 (∃x)

結合子

• -> — 含意 (→)
• <-> — 双条件 (↔)
• & — 連言 (∧)
• | — 選言 (∨)
• - — 否定 (¬)

述語と項

• 述語: man(x)、loves(x, y)、greater(x, y)
• 定数: socrates、a、b
• 変数: x、y、z (小文字、通常は単一の文字)
• 関数: f(x)、successor(n)
• 等値: x = y

例

# すべての人間は死ぬ、ソクラテスは人間
all x (man(x) -> mortal(x))
man(socrates)

# 誰かが誰もが好きな人が存在する
exists x all y loves(x, y)

# 大なりの推移性
all x all y all z ((greater(x, y) & greater(y, z)) -> greater(x, z))

ツールの使用例

1. 定理の証明 (エンジン選択付き)

{
  "name": "prove",
  "arguments": {
    "premises": [
      "all x (man(x) -> mortal(x))",
      "man(socrates)"
    ],
    "conclusion": "mortal(socrates)",
    "engine": "prolog"
  }
}

2. SATエンジンでの証明 (非ホーン式)

{
  "name": "prove",
  "arguments": {
    "premises": ["alpha | beta", "alpha -> gamma", "beta -> gamma"],
    "conclusion": "gamma",
    "engine": "sat"
  }
}

3. 反例の探索

{
  "name": "find-counterexample",
  "arguments": {
    "premises": ["P(a)"],
    "conclusion": "P(b)"
  }
}

4. セッションベースの推論

// 1. セッションを作成する
{ "name": "create-session", "arguments": { "ttl_minutes": 30 } }

// 2. 前提を追加する
{ "name": "assert-premise", "arguments": { 
    "session_id": "abc-123...", 
    "formula": "all x (man(x) -> mortal(x))" 
}}

// 3. 知識ベースをクエリする
{ "name": "query-session", "arguments": { 
    "session_id": "abc-123...", 
    "goal": "mortal(socrates)" 
}}

// 4. クリーンアップ
{ "name": "delete-session", "arguments": { "session_id": "abc-123..." } }

🔧 技術詳細

エンジン連携

EngineManager は自動的に最適なエンジンを選択します:

1. 式の分析 — 入力をクロージファイケーションして構造を決定します。
2. ホーンチェック — すべての節がホーン節の場合、Prologを使用します。
3. SATフォールバック — 非ホーン式はMiniSatにルーティングされます。
4. 明示的な上書き — engine パラメータで特定のエンジンを強制的に選択します。

CNFクロージファイケーション

クロージファイケータは任意の一階論理をCNFに変換します:

1. 双条件と含意を削除します。
2. 否定を内側に押し込みます (NNF)。
3. 変数名を標準化します。
4. 存在量化子をスコレマイズします。
5. 全称量化子を削除します。
6. ORをANDに分配します。
7. 節を抽出します。

DIMACSエクスポート

外部のSATソルバーとの相互運用性のため:

import { clausify, clausesToDIMACS } from './clausifier';

const result = clausify('(P -> Q) & P');
const dimacs = clausesToDIMACS(result.clauses);
// dimacs.dimacs = "p cnf 2 2\n-1 2 0\n1 0"
// dimacs.varMap = Map { 'P' => 1, 'Q' => 2 }

構造化エラー

すべてのエラーには機械可読な情報が含まれています:

interface LogicError {
  code: LogicErrorCode;    // 'PARSE_ERROR' | 'INFERENCE_LIMIT' | ...
  message: string;
  span?: { start, end, line, col };
  suggestion?: string;
  context?: string;
}

📚 詳細ドキュメント

prove

interface ProveArgs {
  premises: string[];
  conclusion: string;
  inference_limit?: number;     // 最大ステップ数 (デフォルト: 1000)
  engine?: 'prolog' | 'sat' | 'auto';  // エンジン選択
  enable_arithmetic?: boolean;  // 算術述語を有効にする
  enable_equality?: boolean;    // 等値公理を注入する
  verbosity?: 'minimal' | 'standard' | 'detailed';
}

interface ProveResult {
  success: boolean;
  result: 'proved' | 'failed' | 'timeout' | 'error';
  message?: string;
  engineUsed?: string;          // 使用されたエンジン
  bindings?: Record<string, string>[];
  proof?: string[];
  prologProgram?: string;       // (詳細モードのみ)
  statistics?: { timeMs: number; inferences?: number };
}

check-well-formed

interface CheckArgs {
  statements: string[];
  verbosity?: 'minimal' | 'standard' | 'detailed';
}

interface ValidationResult {
  valid: boolean;
  formulaResults: Array<{
    formula: string;
    valid: boolean;
    errors: string[];
    warnings: string[];
  }>;
}

find-model / find-counterexample

interface FindModelArgs {
  premises: string[];
  domain_size?: number;
  max_domain_size?: number;     // デフォルト: 10
  verbosity?: 'minimal' | 'standard' | 'detailed';
}

interface ModelResult {
  success: boolean;
  result: 'model_found' | 'no_model' | 'timeout' | 'error';
  model?: {
    domainSize: number;
    predicates: Record<string, string[]>;
    constants: Record<string, number>;
  };
}

セッションツール

// create-session
{ session_id: string; expires_at: string; ttl_minutes: number }

// assert-premise
{ success: boolean; premise_count: number }

// query-session
{ success: boolean; result: string; engineUsed?: string }

// list-premises
{ premises: string[]; premise_count: number }

📄 ライセンス

MIT

🤝 コントリビューション

1. リポジトリをフォークします。
2. 機能ブランチを作成します。
3. テストを実行します: npm test
4. プルリクエストを送信します。