MCP-Logic 服务器

一个提供自动化推理能力的MCP服务器，使用Prover9/Mace4为AI系统提供逻辑推理功能。该服务器通过简洁的MCP接口实现定理证明和逻辑模型验证。

设计理念

MCP-Logic通过专门针对AI系统的接口设计，填补了AI与形式逻辑之间的鸿沟。其独特之处在于：

• AI优先设计：专为AI系统打造，支持自动化推理
• 知识验证：能够对知识表示及其逻辑推论进行正式验证
• 无缝集成：与模型上下文协议（MCP）生态系统完美兼容
• 深度推理：支持复杂逻辑证明，包括嵌套量词和多前提推理
• 实际应用：特别适用于AI知识模型和推理链的验证

功能特点

• 与Prover9无缝集成，支持定理自动证明
• 支持复杂的逻辑公式和证明
• 内置语法验证功能
• 搭配有MCP协议的干净服务器接口
• 具备完善的错误处理和日志记录
• 支持知识表示及AI系统的推理分析

快速示例

# 证明理解加上上下文能够应用于实际
if __name__ == "__main__":
    knowledge = [
        "所有人类都是有生命的生物。",          # 前提1：man(x) → mortal(x)
        "苏格拉底是人。"                        # 前提2：man(socrates)
    ]
    conclusion = "苏格拉底是有生命的。"
    run_knowledge_to_application(knowledge, conclusion)

输出结果

所有人类都是有生命的生物。  # 前提1：man(x) → mortal(x)
苏格拉底是人。             # 前提2：man(socrates)
结论：苏格拉底是有生命的。   # 结论：mortal(socrates)
证明过程：
1. 根据前提1，人类的定义决定了所有人类都是有生命的。
2. 前提2指出苏格拉底属于人类范畴。
3. 因此，通过逻辑推理得出苏格拉底是有生命的结论。

安装说明

系统要求

• 操作系统：Linux/macOS/Windows
• 内存：建议至少4GB RAM
• 磁盘空间：至少10GB可用空间

安装步骤

# 下载项目源码
git clone https://github.com/yourusername/mcp-logic.git
cd mcp-logic

# 运行设置脚本（根据系统选择对应脚本）
# 对于Linux/macOS：
./setup-script.sh

# 对于Windows：
./setup-script.bat

# 安装完成后，生成ladr目录包含Prover9二进制文件

可用工具

工具调用示例

1. 定理证明工具

{
  "tool": "prove-theorem",
  "arguments": {
    "premises": [
      "所有人类都是有生命的生物。",
      "苏格拉底是人。"
    ],
    "conclusion": "苏格拉底是有生命的。"
  }
}

2. 语法验证工具

{
  "tool": "check-well-formed",
  "arguments": {
    "statements": [
      "所有人类都是有生命的生物。",
      "苏格拉底是人。"
    ]
  }
}

文档资料

查看Documents文件夹中的详细分析和示例：

• 知识到应用：关于理解与实际应用在AI系统中的形式逻辑分析

项目结构

mcp-logic/
├── src/
│   └── mcp_logic/
│       └── server.py           # 主MCP服务器实现文件
├── tests/
│   ├── test_proofs.py          # 核心功能测试用例
│   └── test_debug.py           # 调试工具测试
├── Documents/                  # 分析与文档资料
├── pyproject.toml              # Python包配置文件
├── setup-script.sh             # 设置脚本（安装LADR及依赖）
├── run-mcp-logic.sh            # 基于Docker运行脚本（Linux/macOS）
├── run-mcp-logic.bat           # 基于Docker运行脚本（Windows）
├── run-mcp-logic-local.sh      # 本地运行脚本（无Docker）
└── README.md                   # 该项目说明文档

注：运行设置脚本后，会在项目目录下生成一个ladr文件夹，其中包含Prover9二进制文件，但该文件夹不会被纳入仓库版本控制。

开发指南

运行测试用例

uv pip install pytest
uv run pytest

许可证

本项目采用MIT许可证。