MCP-Logic

MCP-Logic

一个使用 Prover9、Mace4 和内置推理大模型进行自动一阶逻辑推理的 MCP 服务。

功能

• 定理证明 - 使用 Prover9 证明逻辑陈述
• 模型查找 - 使用 Mace4 查找有限模型
• 反例查找 - 展示陈述为何不成立
• 语法验证 - 预先验证公式并提供实用的错误消息
• 范畴推理 - 内置范畴论证明支持
• 命题偶然性 - 纯分析型 HCC 证明器，可快速检查命题
• 溯因推理 - 使用变分自由能（VFE）为假设排序
• 🤖 逻辑顾问（新功能） - 内置的 TwIL-LM3 推理大模型，可端到端解决逻辑问题：只需用自然语言提问
• 独立运行 - 所有依赖项都会自动安装

快速开始

安装

Linux/macOS：

git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
./linux-setup-script.sh

Windows：

git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
windows-setup-mcp-logic.bat

设置脚本会自动：

• 下载并构建 LADR（Prover9 + Mace4）
• 创建 Python 虚拟环境
• 安装所有依赖项
• 生成 Claude Desktop 配置

启用逻辑顾问（可选）

内置逻辑顾问使用本地的 3B 参数大模型（TwIL-LM3 Q8）端到端解决逻辑问题。运行设置脚本即可安装：

Linux/macOS：

./setup-advisor.sh

Windows：

setup-advisor.bat

脚本会自动：

• 检测你的 GPU — NVIDIA 上的 CUDA（Linux/Windows）、Apple Silicon 上的 Metal（macOS），或回退到 CPU
• 使用正确的加速后端编译 llama-cpp-python
• 下载模型（约 3.3 GB，仅需一次）到 ~/.cache/mcp-logic/models/

无需激活 venv — 设置脚本使用 uv 自动管理虚拟环境。所有 uv run 和 uv pip install --directory 命令都会在无需事先激活的情况下，针对项目的 .venv 执行。

手动安装（进阶）

如果你更愿意手动安装，而不使用设置脚本：

Linux（NVIDIA GPU）：

CMAKE_ARGS="-DGGML_CUDA=on" uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

macOS（Apple Silicon）：

CMAKE_ARGS="-DGGML_METAL=on" uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

Windows（NVIDIA GPU，PowerShell）：

$env:CMAKE_ARGS="-DGGML_CUDA=on"
uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

仅使用 CPU（任意平台）：

uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

模型会在首次使用时自动下载，也可以提前手动下载：

uv run --directory . python -c "
from huggingface_hub import hf_hub_download
hf_hub_download('webAI-Official/TwIL-LM3', 'TwIL-LM3-Q8_0.gguf',
                revision='5d90f3a3251e142fc5cc6b42a62b175fdb0d4ccd',
                local_dir='$HOME/.cache/mcp-logic/models',
                local_dir_use_symlinks=False)
"

平台兼容性

平台	GPU 加速	说明
Linux（x86_64）	✅ CUDA（NVIDIA）	需要 CUDA Toolkit + nvidia-smi
macOS（Apple Silicon）	✅ Metal	建议使用原生 ARM64 Python
macOS（Intel）	⚠️ Metal（有限）	可以运行，但速度比 Apple Silicon 慢
Windows（x86_64）	✅ CUDA（NVIDIA）	需要 CUDA Toolkit + Visual Studio Build Tools
任意平台	✅ CPU	始终可用，但速度较慢（3B 模型每次查询约需 10-20 秒）

Claude Desktop 集成

将以下内容添加到 Claude Desktop MCP 配置中（自动生成于 claude-app-config.json）：

{
  "mcpServers": {
    "mcp-logic": {
      "command": "uv",
      "args": [
        "--directory",
        "/absolute/path/to/mcp-logic",
        "run",
        "mcp_logic",
        "--prover-path",
        "/absolute/path/to/mcp-logic/ladr/bin"
      ]
    }
  }
}

重要： 将 /absolute/path/to/mcp-logic 替换为实际的仓库路径。

添加 "--no-advisor" 可进行确定性的纯求解器测试，或在未安装可选顾问依赖项时使用。模型采用延迟加载，因此常规的 prove 和 find_model 调用不会占用 GPU 内存。

Codex 集成

使用绝对路径全局注册 stdio 服务：

codex mcp add mcp-logic -- \
  /absolute/path/to/mcp-logic/.venv/bin/mcp_logic \
  --prover-path /absolute/path/to/mcp-logic/ladr/bin

使用 codex mcp get mcp-logic 确认保存的命令。添加或更改服务后，重启 Codex，以便在下个会话中加载其工具。

可用工具

工具	用途
ask_logic_advisor 🤖	用通俗英语解决逻辑问题（端到端）
prove	使用 Prover9 证明陈述
check_well_formed	验证公式语法，并提供详细错误信息
find_model	查找满足前提条件的有限模型
find_counterexample	查找反例，表明结论无法推出
verify_commutativity	为范畴图的交换性生成一阶逻辑公式
get_category_axioms	获取范畴／函子／群／幺半群的公理
check_contingency	使用 HCC 证明器检查真值函数的偶然性
abductive_explain	查找使 VFE 最小化的观测解释

使用示例

询问逻辑顾问（最简单）

只需用自然语言提出问题——顾问会将其形式化、运行求解器，并解释结果：

Use ask_logic_advisor with:
question: "Is it true that if all humans are mortal and Socrates is human,
           then Socrates is mortal?"

结果： 顾问将其转换为一阶逻辑公式，使用 Prover9 证明定理，并返回：

“是的，苏格拉底会死。该证明基于‘所有人都会死’这一全称前提，以及苏格拉底是人的事实。”

响应还会包含所用的形式化内容和原始求解器输出，以供查验。

证明定理（直接方式）

Use the prove tool with:
premises: ["all x (man(x) -> mortal(x))", "man(socrates)"]
conclusion: "mortal(socrates)"

结果： ✓ 定理已证明

分析命题逻辑的偶然性

Use the check_contingency tool with:
formula: "(p -> q) | (q -> p)"

结果： 确定该公式是一个非偶然的重言式，并返回证明过程。

查找反例

Use the find_counterexample tool with:
premises: ["P(a)"]
conclusion: "P(b)"

结果： 找到一个模型，其中 P(a) 为真而 P(b) 为假，证明结论无法推出。

验证范畴图

Use the verify_commutativity tool with:
path_a: ["f", "g"]
path_b: ["h"]
object_start: "A"
object_end: "C"

结果： 给出一阶逻辑前提和结论，以证明 f∘g = h。

在本地运行

无需使用 Claude Desktop，可直接运行服务：

Linux/macOS：

./run_mcp_logic.sh

Windows：

run_mcp_logic.bat

项目结构

mcp-logic/
├── src/mcp_logic/
│   ├── server.py              # Main MCP server (9 tools)
│   ├── logic_advisor.py       # Onboard TwIL-LM3 agentic solver
│   ├── mace4_wrapper.py       # Mace4 model finder
│   ├── syntax_validator.py    # Formula syntax validation
│   ├── categorical_helpers.py # Category theory utilities
│   ├── hcc_prover.py          # Hypersequent Contingency Calculus prover
│   ├── vfe_engine.py          # Variational Free Energy abductive engine
│   ├── formula_ast.py         # Propositional logic AST and parser
│   └── fol_ast.py             # First-order AST, parser, and transformations
├── ladr/                      # Auto-installed Prover9/Mace4 binaries
│   └── bin/
│       ├── prover9
│       └── mace4
├── tests/                     # Unit, solver integration, and MCP stdio tests
├── linux-setup-script.sh      # Linux/macOS core setup
├── windows-setup-mcp-logic.bat # Windows core setup
├── setup-advisor.sh           # Linux/macOS advisor setup
├── setup-advisor.bat          # Windows advisor setup
├── run_mcp_logic.sh           # Linux/macOS run script
└── run_mcp_logic.bat          # Windows run script

逻辑顾问详情

ask_logic_advisor 工具采用一个由 3 个阶段组成的 Agent 式流水线：

  Natural Language Question
         │
         ▼
  ┌─────────────────────┐
  │ 1. FORMALIZE        │  TwIL-LM3 translates to FOL
  │    (LLM call)       │  → {"tool":"prove", "premises":[...], ...}
  └────────┬────────────┘
           ▼
  ┌─────────────────────┐
  │ 2. EXECUTE          │  Runs actual Prover9/Mace4/HCC
  │    (Solver call)    │  → {"result":"proved", "proof":...}
  └────────┬────────────┘
           ▼
  ┌─────────────────────┐
  │ 3. INTERPRET        │  TwIL-LM3 explains the result
  │    (LLM call)       │  → Plain English answer
  └─────────────────────┘

• 模型：TwIL-LM3（30 亿参数，针对形式推理微调）
• 量化：Q8_0 GGUF（磁盘占用约 3.3 GB，显存占用约 3.5 GB）
• 延迟加载：模型在首次查询时加载，而非在服务启动时加载
• 许可证：webAI 非商业许可证 v1.0（仅限非商业用途）

资源需求

场景	显存	推理速度
NVIDIA GPU（CUDA）	约 3.5 GB	每次大模型调用约 1-3 秒
Apple Silicon（Metal）	约 3.5 GB	每次大模型调用约 2-5 秒
仅 CPU	0（使用 RAM）	每次大模型调用约 10-20 秒

v0.4.0 新增内容

内置逻辑顾问：

• ✅ ask_logic_advisor 工具：用通俗英语解决逻辑问题——内置的 TwIL-LM3 大模型会自动将问题形式化、运行求解器并解读结果
• ✅ 跨平台 GPU 设置：自动检测 CUDA（NVIDIA）或 Metal（Apple Silicon），并据此进行编译
• ✅ 延迟加载模型：首次调用顾问前不会占用显存
• ✅ 自动下载：首次使用时从 HuggingFace 下载模型

v0.3.0 新增内容

认知架构增强：

• ✅ 超序列偶然性演算（HCC）： 新增严谨的演绎检查器，无需蛮力建模即可即时评估命题公式的偶然性。
• ✅ 变分自由能（VFE）引擎： 实现溯因推理，使用非教条的 Cournot-Gaifman 先验对假设排序，从而优雅地满足奥卡姆剃刀原则。
• ✅ 智能证明器路由： prove 工具会自动将纯命题查询路由到 HCC 引擎，将一阶查询路由到 Prover9。
• ✅ 可配置的模型查找器： find_model 和 find_counterexample 现已支持自定义超时，以及结构化的谓词／函数提取。
• ✅ 可判定片段搜索： BSR 和安全有界的单子理论 会执行完整的 1..model_bound 搜索。只有在上下文许可的 PROVED 或 REFUTED 状态下，no_model_found 响应 才具有确定性；BOUNDED_NO_MODEL 响应仍保留有限界限带来的不确定性。
• ✅ 面向理论的顾问路由： 求解器选择依据解析后的公式结构， 包括混合算术和无解释谓词，而非英语关键词匹配。
• ✅ 变量作用域检查： check_well_formed 会警告隐式全称量化 和未使用的绑定变量，但不会拒绝合法的 Prover9 公式。

v0.2.0 新增内容

功能增强：

• ✅ Mace4 模型查找和反例检测
• ✅ 详细的语法验证，并提供特定位置的错误信息
• ✅ 支持范畴推理（范畴论公理、交换性验证）
• ✅ 所有工具均提供结构化 JSON 输出
• ✅ 安装过程自包含（无需手动配置路径）

开发

测试夹具会自动查找随附的 ladr/bin/prover9 和 ladr/bin/mace4；正常检出代码库时无需设置 LADR_PATH。

运行完整测试套件：

.venv/bin/python -m pytest tests/ -q

仅运行端到端 MCP stdio 测试。该测试会启动服务，并通过 MCP 工具调用测试 Prover9 和 Mace4：

.venv/bin/python -m pytest tests/test_mcp_stdio_integration.py -q

受限的进程沙箱可能允许 LADR 二进制文件启动，却阻止其继续运行，从而产生误导性的 30/60 秒 超时。请在沙箱外运行依赖求解器的测试；不要通过增加求解器超时来应对。

文档

• mcp_logic_agent.md - Agent 指南（工具参考 + 工作流）
• ENHANCEMENTS.md - v0.2.0 功能速查
• Documents/ - 详细分析和示例

故障排除

“Prover9 not found”错误：

• 运行设置脚本：./linux-setup-script.sh 或 windows-setup-mcp-logic.bat
• 检查 ladr/bin/prover9 和 ladr/bin/mace4 是否存在

逻辑顾问无法正常工作：

• 运行顾问设置脚本：./setup-advisor.sh 或 setup-advisor.bat
• 检查 GPU 检测情况：nvidia-smi（Linux/Windows）或 system_profiler SPDisplaysDataType（macOS）
• 强制使用 CPU 模式：./setup-advisor.sh --cpu
• 检查模型是否存在：ls ~/.cache/mcp-logic/models/TwIL-LM3-Q8_0.gguf
• 如果不需要，请禁用：在服务参数中添加 --no-advisor

“llama-cpp-python”构建失败：

• Linux：安装构建工具：sudo apt-get install build-essential cmake
• macOS：安装 Xcode 工具：xcode-select --install
• Windows：安装 Visual Studio Build Tools，并选择“Desktop development with C++”工作负载
• CUDA：确保已安装 CUDA Toolkit，且 nvcc 位于 PATH 中

服务未更新：

• 代码变更后重启服务
• 检查日志中的语法错误

语法验证警告：

• 谓词／函数名使用小写（例如，man(x) 而不是 Man(x)）
• 在运算符两侧添加空格，以提高可读性
• 确保所有括号均成对

许可证

MIT（mcp-logic server）

**注意：**逻辑顾问使用的 TwIL-LM3 模型采用 webAI 非商业许可证 v1.0。这意味着顾问功能仅限非商业用途。核心 mcp-logic server（prove、find_model 等）仍采用 MIT 许可证，可用于商业用途，无需使用顾问功能。

致谢

• Prover9/Mace4：William McCune 的 LADR 库
• LADR 仓库：laitep/ladr
• TwIL-LM3：webAI — 针对形式逻辑微调的 3B 推理模型
• 超序贯式偶然性演算（HCC）：基于 Eugenio Orlandelli、Giannandrea Pulcini 和 Achille C. Varzi 于 2024 年发表的《A Hypersequent Calculus for Classical Contingencies》。