mcplogic (Automenta)

MCP逻辑

一个用于一阶逻辑推理的自包含MCP服务器，用TypeScript实现，没有外部二进制依赖关系。

原件：https://github.com/angrysky56/mcp-logic/

______________________________________________________________________

功能状态

✅ = 已实施|🔲 = 计划|🔬 = 研究/愿景

核心推理

• \[x\] 定理证明 --通过Tau Prolog进行基于分辨率的证明
• \[x\] 模型查找 --有限模型枚举（SAT域≤25）
• \[x\] 反例检测 --找到反驳结论的模型
• \[x\] 语法验证 --预先验证有详细错误的公式
• \[x\] CNF分层 --将FOL转换为结膜范式
• \[x\] 网站转换 --SAT的线性尺寸CNF转换（避免指数膨胀）
• \[x\] DIMACS导出 --为外部SAT求解器导出CNF
• \[x\] 对称性破坏 --Lex leader用于模型搜索（以指数方式减少搜索空间）
• \[x\] SAT支持的模型查找 --使用自动SAT阈值扩展到25+域
• \[ \] 同构滤波 --跳过等效模型（推迟到“findAllModels”用例）
• \[x\] 证据痕迹 --逐步推导输出（通过 include_trace)

发动机联合会

• \[x\] 多引擎架构 --发动机自动选择
• \[x\] Prolog引擎 （Tau-Prolog）——Horn子句、数据日志、等式
• \[x\] SAT发动机 （MiniSat）——一般FOL，非喇叭公式
• \[x\] SMT引擎 （Z3）——带算术和量词的高性能SMT求解器
• \[x\] ASP引擎 （Clingo）——答案集编程（约束与模型）
• \[x\] 发动机参数 --通过以下方式明确选择发动机 engine 参数
• \[x\] 迭代深化 --复杂证明的渐进推理极限策略
• \[x\] 资源管理 --自动清理WASM资源（Z3上下文）
• \[ \] 证明人9 WASM --可选的高功率ATP（推迟到SAT+迭代证明不足时）
• \[ \] 解调 --等式项重写（推迟到等式工作负载显示性能问题时）

逻辑特性

• \[x\] 算术支持 --内置： lt, gt, plus, minus, times, divides
• \[x\] 平等推理 --反射性、对称性、传递性、相合性
• \[x\] 重写系统 --Knuth-Bendix风格的术语重写，以实现高效的等式处理（Prolog）
• \[x\] 扩展公理库 --环、场、格、等价关系公理
• \[x\] 功能解释 --模型查找的全功能支持
• \[ \] 键入/排序的FOL --域约束类型注释（研究）
• \[ \] 模态逻辑 --必要性、可能性运算符（研究）
• \[ \] 概率逻辑 --加权事实，贝叶斯推理（研究）

MCP协议

• \[x\] 基于会话的推理 --基于资源清理的增量知识库构建
• \[x\] Axiom资源 --可浏览库（类别、皮亚诺、ZFC、环、格等）
• \[x\] 推理提示 --校样模板
• \[x\] 详细程度控制 — minimal/standard/detailed 回复
• \[x\] 结构化错误 --机器可读错误代码和建议
• \[x\] 流媒体进度 --实时进度通知（通过MCP通知）
• \[x\] 高功率模式 --带警告的扩展限制（通过 highPower 选项）

先进发动机

• \[x\] SMT（Z3 WASM） --理论推理（算术、数组）、等式、量词。
• \[x\] ASP（Clingo） --非单调推理、默认值、偏好。
• \[ \] 神经引导 --LLM建议的验证路径
• \[ \] 高阶逻辑 --量化谓词（研究）

测试和基准

• \[x\] 单元测试 --265+项测试通过，80%+覆盖率
• \[x\] 造粒机问题 --P1-P10基准测试套件（可扩展到P1-P75）
• \[x\] 对称性基准 --贝尔编号验证测试
• \[x\] SAT模型测试 --群论与代数结构验证
• \[x\] 弹性测试 --资源泄漏检测和复杂性限制验证
• \[ \] TPTP库子集 --标准ATP基准

______________________________________________________________________

快速开始

安装

git clone 
cd mcplogic
pnpm install
pnpm run build

运行服务器

pnpm start

验证

运行全面的健康检查以验证构建、测试和发动机可用性：

pnpm run verify

克劳德桌面/MCP客户端配置

添加到MCP配置中：

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

CLI工具

该软件包包括一个用于离线使用和验证的CLI：

# Check engine status
mcplogic check

# Prove a theorem from a file
mcplogic prove problem.p

# Find a model
mcplogic model theory.p

# Interactive REPL
mcplogic repl

______________________________________________________________________

可用工具

核心推理工具

会话管理工具

______________________________________________________________________

引擎选择

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

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

这 include_trace 选项（boolean）允许在响应中逐步导出输出，这对于调试或理解证明路径非常有用。

发动机性能

______________________________________________________________________

公式语法

此服务器使用与Prover9兼容的一阶逻辑（FOL）语法：

量词

• all x (...) --通用量化（∀x）
• exists x (...) --存在量化（∃x）

连接词

• -> --含义（→）
• `` --空调(↔)
• & --共轭（∧）
• | --断开（∨）
• - --否定（¬）

例子

# All men are mortal, Socrates is a man
all x (man(x) -> mortal(x))
man(socrates)

# Transitivity of greater-than
all x all y all z ((greater(x, y) & greater(y, z)) -> greater(x, z))

______________________________________________________________________

MCP资源

______________________________________________________________________

详细程度控制

所有工具均支持 verbosity 参数：

______________________________________________________________________

限制（当前）

1. 模型大小 --查找器仅限于≤25个元素的域（使用SAT）
2. 推理深度 --复杂证明可能超过默认限制（通过以下方式增加 inference_limit 或使用 iterative 战略）
3. 高阶 --仅支持一阶逻辑

未来的改进可能会根据实际使用情况来解决这些限制。

______________________________________________________________________

发展

pnpm run build     # Compile TypeScript
pnpm test          # Run test suite
pnpm run dev       # Development mode with auto-reload

______________________________________________________________________

许可证

麻省理工学院

______________________________________________________________________

未来方向

潜在的增强功能将由实际使用情况驱动：

• 同构滤波 --跳过穷举模型枚举中的等效模型
• \[x\] 证据痕迹 --教育/调试用例的逐步推导输出
• 解调 --等式重载工作负载的等式项重写优化
• \[x\] 流媒体进度 --长时间运行操作的实时进度通知
• 扩展基准 --TPTP库子集和群论问题集
• \[x\] 先进发动机 --SMT（Z3）、ASP（Clingo）
• \[x\] 进化引擎 --进化高效证明策略的遗传算法
• \[ \] 神经引导 --LLM建议的验证路径

故障排除

WASM发动机（Z3/Clingo）

如果您遇到与以下内容相关的错误 z3-solver 或 clingo-wasm:

1. 确保您的环境支持WebAssembly。
2. 在浏览器环境中，确保 .wasm 文件已正确送达。这 check 命令可以验证Node.js中的基本功能。
3. 如果你看到 OOM 或者内存错误，请尝试使用默认引擎（Prolog）运行或增加超时/推理限制。

构建：浏览器故障

确保你已经跑步了 pnpm install 获取最新的类型定义。浏览器构建依赖于在中处理的WASM模块的特定覆盖 src/engines/*/index.ts.