MCP Logic

🚀 MCP-Logic 服务器

MCP-Logic 服务器是一个提供自动化推理能力的MCP服务器，借助 Prover9/Mace4 为 AI 系统赋予逻辑推理功能。它通过简洁的 MCP 接口，实现定理证明和逻辑模型验证，极大地提升了 AI 系统在逻辑推理方面的效率和准确性。

🚀 快速开始

MCP-Logic 通过专门针对 AI 系统的接口设计，填补了 AI 与形式逻辑之间的鸿沟。以下是一个快速示例，展示如何使用 MCP-Logic 进行逻辑推理：

# 证明理解加上上下文能够应用于实际
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. 因此，通过逻辑推理得出苏格拉底是有生命的结论。

✨ 主要特性

• AI优先设计：专为 AI 系统打造，支持自动化推理，让 AI 系统能够更高效地进行逻辑推理。
• 知识验证：能够对知识表示及其逻辑推论进行正式验证，确保知识的准确性和可靠性。
• 无缝集成：与模型上下文协议（MCP）生态系统完美兼容，方便与其他系统进行集成。
• 深度推理：支持复杂逻辑证明，包括嵌套量词和多前提推理，满足各种复杂场景的需求。
• 实际应用：特别适用于 AI 知识模型和推理链的验证，为 AI 系统的实际应用提供有力支持。
• 与 Prover9 无缝集成，支持定理自动证明，提高证明效率。
• 支持复杂的逻辑公式和证明，处理各种复杂的逻辑问题。
• 内置语法验证功能，确保输入的逻辑公式符合语法规则。
• 搭配有 MCP 协议的干净服务器接口，提供简洁易用的接口。
• 具备完善的错误处理和日志记录，方便调试和维护。
• 支持知识表示及 AI 系统的推理分析，助力 AI 系统的开发和优化。

📦 安装指南

系统要求

• 操作系统：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 许可证。