MCP Logic

MCP逻辑


使用Prover9和Mace4进行自动一阶逻辑推理的MCP服务器。

特性

• 定理证明 -用Prover9证明逻辑语句
• 模型查找 -使用Mace4查找有限模型
• 反例发现 -说明为什么陈述不成立
• 语法验证 -使用有用的错误消息对公式进行预验证
• 范畴推理 -内置对范畴理论证明的支持
• 命题应急 -用于快速命题检查的纯分析HCC证明器
• 溯因推理 -使用变分自由能（VFE）对假设进行排序
• 独立 -所有依赖项都会自动安装

快速开始

安装

Linux/macOS：

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

窗户：

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

安装脚本会自动执行以下操作：

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

Claude桌面集成

添加到您的Claude Desktop MCP配置（自动生成于 claude-app-config.json):

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

重要提示： 替换 /absolute/path/to/mcp-logic 使用您的实际存储库路径。

可用工具

示例用法

证明一个定理

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

结果： ✓ 定理证明

分析命题偶然性

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

结果： 标识公式为非条件公式 同义反复，返回证明痕迹。

查找反例

Use the mcp-logic find-counterexample tool with:
premises: ["P(a)"]
conclusion: "P(b)"

结果： 模型在哪里找到 P(a) 确实如此，但 P(b) 是错误的，证明结论不成立。

验证分类图

Use the mcp-logic verify-commutativity tool with:
path_a: ["f", "g"]
path_b: ["h"]
object_start: "A"
object_end: "C"

结果： FOL前提和结论证明 f∘g = h.

本地运行

直接运行服务器而不是Claude Desktop：

Linux/macOS：

./run_mcp_logic.sh

窗户：

run_mcp_logic.bat

项目结构

mcp-logic/
├── src/mcp_logic/
│   ├── server.py              # Main MCP server (8 tools)
│   ├── 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
├── ladr/                      # Auto-installed Prover9/Mace4 binaries
│   └── bin/
│       ├── prover9
│       └── mace4
├── tests/                     # Test suite
├── linux-setup-script.sh      # Linux/macOS setup
├── windows-setup-mcp-logic.bat # Windows setup
├── run_mcp_logic.sh           # Linux/macOS run script
└── run_mcp_logic.bat          # Windows run script

v0.3.0的新增功能

认知架构增强：

• ✅ 高频权变演算（HCC）： 添加了一个严格的演绎检查器，用于在没有暴力建模的情况下立即评估命题公式的偶然性。
• ✅ 可变自由能（VFE）发动机： 实现了溯因推理，在优雅地满足奥卡姆剃刀之前，使用非教条的古诺-盖夫曼对假设进行排序。
• ✅ 智能验证路由： prove 该工具自动将纯命题查询路由到HCC引擎，并将一阶查询路由到Prover9。
• ✅ 可配置模型查找器： find_model 和 find_counterexample 现在支持自定义超时和结构化谓词/函数提取。

v0.2.0的新增功能

增强功能：

• ✅ Mace4模型发现和反例检测
• ✅ 带有特定位置错误的详细语法验证
• ✅ 范畴推理支持（范畴论公理、交换性验证）
• ✅ 所有工具的结构化JSON输出
• ✅ 独立安装（无需手动路径配置）

发展

运行测试：

source .venv/bin/activate
pytest tests/ -v

直接测试组件：

python tests/test_enhancements.py

文档

• ENHANCEMENTS.md -v0.2.0功能的快速参考
• Documents/ -详细分析和示例
• walkthrough.md -实施细节（以工件形式）

故障排除

“未找到Prover9”错误：

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

服务器未更新：

• 代码更改后重新启动服务器
• 检查日志是否存在语法错误

语法验证警告：

• 谓词/函数使用小写（例如。， man(x) 不 Man(x))
• 为清楚起见，在运算符周围添加空格
• 平衡所有括号

许可证

麻省理工学院

学分

• Prover9/Mace4：威廉·麦卡恩的LADR图书馆
• LADR存储库: laitep/ladr
• 高频权变演算（HCC）：基于Eugenio Orlandelli、Giannandrea Pulcini和Achille C.Varzi（2024）的“经典偶然性的超序列微积分”的逻辑框架。