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	使用归结法并选择引擎证明语句
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. 提交拉取请求。