shield_lock
JinDaGe
← Back to MCP directory
publicPublicdnsLocal runtime

mcplogic

一个自包含的MCP服务器，用于一阶逻辑推理，支持定理证明、模型查找和反例检测，采用多引擎架构自动选择最佳推理引擎。

article

README

🚀 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 | 使用归结法并选择引擎证明语句 | | check-well-formed | 验证公式语法并提供详细错误信息 | | find-model | 查找满足前提条件的有限模型 | | find-counterexample | 查找表明语句不成立的反例 | | verify-commutativity | 生成范畴图交换性的一阶逻辑公式 | | get-category-axioms | 获取范畴/函子/幺半群/群的公理 |

会话管理工具

| 工具 | 描述 | |------|-------------| | create-session | 创建具有生存时间（TTL）的新推理会话 | | assert-premise | 将会话的知识库中添加一个公式 | | query-session | 使用目标查询累积的知识库 | | retract-premise | 从知识库中移除特定前提 | | list-premises | 列出会话中的所有前提 | | clear-session | 清除所有前提（保持会话活动） | | delete-session | 完全删除会话 |

引擎选择

prove工具支持自动或显式选择引擎：

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

| 引擎 | 适用场景 | 功能 | |--------|----------|--------------| | prolog | Horn子句、Datalog | 等式、算术、高效合一 | | sat | 非Horn公式、SAT问题 | 完整的一阶逻辑、CNF求解 | | 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资源协议浏览公理库： | 资源URI | 描述 | |--------------|-------------| | logic://axioms/category | 范畴论公理 | | logic://axioms/monoid | 幺半群结构 | | logic://axioms/group | 群公理 | | logic://axioms/peano | 皮亚诺算术 | | logic://axioms/set-zfc | ZFC集合论基础 | | logic://axioms/propositional | 命题重言式 | | logic://templates/syllogism | 亚里士多德三段论模式 | | logic://engines | 可用的推理引擎（JSON格式） |

MCP提示

常见任务的推理模板： | 提示 | 描述 | |--------|-------------| | prove-by-contradiction | 设置反证法证明 | | verify-equivalence | 检查公式等价性 | | formalize | 自然语言到一阶逻辑的翻译指南 | | diagnose-unsat | 诊断不可满足的前提 | | explain-proof | 解释已证明的定理 |

详细程度控制

所有工具都支持verbosity参数： | 级别 | 描述 | 使用场景 | |-------|-------------|----------| | minimal | 仅显示成功/结果 | 高效的大语言模型链 | | standard | 增加消息、绑定、使用的引擎 | 默认平衡 | | detailed | 增加Prolog程序、统计信息 | 调试 |

{
  "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. 提交拉取请求。
help

Runtime guide

cloud

Hosted runtime

Hosted servers run from a provider-managed environment. You usually connect the MCP client to the hosted endpoint or follow the provider's authorization flow, without keeping a local process alive

  1. Open provider connection page
  2. Authorize or copy endpoint
  3. Connect from your MCP client
terminal

Local runtime / other methods

Local servers run on your own machine or infrastructure. You normally copy the server_config into your MCP client, install the required package, and provide env variables from env_schema when needed

  1. Copy server_config
  2. Install required package
  3. Fill env variables and restart client