Mcplogic

🚀 MCP Logic

MCP Logic是一個獨立的一階邏輯推理服務器，用TypeScript實現，無需外部二進制依賴。它能夠進行定理證明、模型查找等多種邏輯推理任務，為邏輯推理提供了便捷的解決方案。

🚀 快速開始

安裝

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

✨ 主要特性

核心推理

• 定理證明：使用歸結法證明邏輯語句。
• 模型查找：查找滿足前提條件的有限模型。
• 反例檢測：查找表明結論不成立的模型。
• 語法驗證：預先驗證公式，並提供詳細的錯誤信息。

引擎聯合

• 多引擎架構：根據公式結構自動選擇引擎。
• Prolog引擎（Tau - Prolog）：對Horn子句、Datalog和等式推理效率高。
• SAT引擎（MiniSat）：處理一般的一階邏輯和非Horn公式。
• 引擎參數：可顯式選擇引擎：'prolog'、'sat'或'auto'。

高級邏輯

• 算術支持：內置謂詞：lt、gt、plus、minus、times、divides。
• 等式推理：包含自反性、對稱性、傳遞性和同餘公理。
• CNF子句化：將一階邏輯轉換為合取範式。
• DIMACS導出：導出CNF以用於外部SAT求解器。

MCP協議

• 基於會話的推理：增量式知識庫構建。
• 公理資源：可瀏覽的公理庫（範疇論、皮亞諾算術、ZFC等）。
• 推理提示：用於反證法證明、形式化等的模板。
• 詳細程度控制：為大語言模型鏈提供高效的響應。

基礎設施

• 獨立運行：僅依賴npm包，無需外部二進制文件。
• 結構化錯誤：提供機器可讀的錯誤信息和建議。
• 254個測試：全面的測試覆蓋。

📦 安裝指南

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

💻 使用示例

基礎用法

1. 證明定理（選擇引擎）

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

2. 使用SAT引擎證明（非Horn公式）

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

📚 詳細文檔

可用工具

核心推理工具

會話管理工具

引擎選擇

prove工具支持自動或顯式選擇引擎：

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

{ "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))

🔧 技術細節

引擎聯合

EngineManager會自動選擇最佳引擎：

1. 公式分析：將輸入子句化以確定結構。
2. Horn檢查：如果所有子句都是Horn子句，則使用Prolog。
3. SAT備用：非Horn公式將路由到MiniSat。
4. 顯式覆蓋：engine參數可強制選擇特定引擎。

CNF子句化

子句化器將任意一階邏輯轉換為CNF：

1. 消除雙條件和蘊含。
2. 向內推否定（NNF）。
3. 標準化變量名。
4. 對存在量詞進行Skolem化。
5. 去掉全稱量詞。
6. 分配析取對合取的運算。
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;
}

📄 API文檔

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 }

⚠️ 侷限性

1. 推理深度：複雜證明可能超出限制。
2. 模型大小：模型查找器僅限於域元素數量 ≤10 的情況。
3. SAT變量：SAT引擎不支持算術。
4. 高階邏輯：僅支持一階邏輯。

🛠️ 故障排除

有效定理顯示“未找到證明”

• 對於複雜證明，增加inference_limit。
• 對於非Horn公式，嘗試engine: 'sat'。
• 如果使用等式，啟用enable_equality。

模型查找器返回“未找到模型”

• 增加max_domain_size。
• 檢查前提是否矛盾。

會話錯誤

• 檢查會話是否未過期（默認：30分鐘）。
• 使用list-premises檢查狀態。

🛠️ 開發

npm test          # 運行254個測試
npm run build     # 編譯TypeScript
npx tsc --noEmit  # 僅進行類型檢查

📄 許可證

MIT

🤝 貢獻

1. 分叉倉庫。
2. 創建功能分支。
3. 運行測試：npm test。
4. 提交拉取請求。