MCP Logic

🚀 MCP-Logic 服务器

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

🚀 快速开始

MCP-Logic服务器专为AI系统设计，通过简洁的MCP接口实现定理证明和逻辑模型验证。以下是一个简单的使用示例，展示如何使用该服务器进行逻辑推理：

# 证明理解加上上下文能够应用于实际
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系统打造，支持自动化推理。
• 知识验证：能够对知识表示及其逻辑推论进行正式验证。
• 无缝集成：与模型上下文协议（MCP）生态系统完美兼容。
• 深度推理：支持复杂逻辑证明，包括嵌套量词和多前提推理。
• 实际应用：特别适用于AI知识模型和推理链的验证。
• 与Prover9无缝集成：支持定理自动证明。
• 支持复杂逻辑：支持复杂的逻辑公式和证明。
• 语法验证：内置语法验证功能。
• 干净接口：搭配有MCP协议的干净服务器接口。
• 完善处理：具备完善的错误处理和日志记录。
• 推理分析：支持知识表示及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二进制文件

💻 使用示例

基础用法

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

📚 详细文档

可用工具

1. 定理证明工具

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

2. 语法验证工具

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

项目结构

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许可证。