MCP-Logic

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

设计理念

MCP-Logic 通过提供一个强大的接口到 Prover9/Mace4，填补了 AI 系统与形式逻辑之间的鸿沟。其特别之处在于：

• 以 AI 为中心的设计：专为 AI 系统进行自动化推理而构建
• 知识验证：支持对知识表示和逻辑蕴含的形式化验证
• 无缝集成：与 Model Context Protocol (MCP) 生态系统无缝集成
• 深度推理：支持包含嵌套量词和多个前提的复杂逻辑证明
• 实际应用：特别适用于验证 AI 知识模型和推理链

功能

• 与 Prover9 无缝集成以实现自动定理证明
• 支持复杂的逻辑公式和证明
• 内置语法验证
• 清晰的 MCP 服务器接口
• 广泛的错误处理和日志记录
• 支持知识表示及关于 AI 系统的推理

快速示例

# Prove that understanding + context leads to application
result = await prove(
    premises=[
        "all x all y (understands(x,y) -> can_explain(x,y))",
        "all x all y (can_explain(x,y) -> knows(x,y))",
        "all x all y (knows(x,y) -> believes(x,y))",
        "all x all y (believes(x,y) -> can_reason_about(x,y))",
        "all x all y (can_reason_about(x,y) & knows_context(x,y) -> can_apply(x,y))",
        "understands(system,domain)",
        "knows_context(system,domain)"
    ],
    conclusion="can_apply(system,domain)"
)
# Returns successful proof!

安装

前提条件

• Python 3.10+
• UV 包管理器
• Git 用于克隆仓库
• CMake 和构建工具（用于构建 LADR/Prover9）

设置

克隆此仓库

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

运行设置脚本：
Windows 运行：

windows-setup-mcp-logic.bat

Linux/macOS：

chmod +x linux-setup-script.sh
./linux-setup-script.sh

设置脚本将执行以下操作：

• 检查依赖项（git, cmake, 构建工具）
• 从外部仓库下载 LADR (Prover9/Mace4): laitep/LADR
• 构建 LADR 库以在 ladr/bin 目录中创建 Prover9 二进制文件
• 创建一个 Python 虚拟环境
• 设置配置文件以便在有或没有 Docker 的情况下运行

重要提示：LADR 目录不包含在此仓库内，将通过设置脚本或手动安装。

使用 Docker - 不确定这是否正确工作，主要设计用于直接与 Claude Desktop 一起使用

如果您更喜欢使用 Docker，此脚本将：

• 查找可用端口
• 激活虚拟环境
• 以正确的路径运行服务器以指向已安装的 Prover9

# Linux/macOS
./run-mcp-logic.sh

# Windows
run-mcp-logic.bat

这些脚本将构建并运行一个具有必要环境的 Docker 容器。

Claude Desktop 集成

要将 MCP-Logic 与 Claude Desktop 一起使用，请使用以下配置：

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

将 "/path/to/mcp-logic" 替换为您实际的仓库路径。

可用工具

prove

使用 Prover9 运行逻辑证明：

{
  "tool": "prove",
  "arguments": {
    "premises": [
      "all x (man(x) -> mortal(x))",
      "man(socrates)"
    ],
    "conclusion": "mortal(socrates)"
  }
}

check-well-formed

验证逻辑语句的语法：

{
  "tool": "check-well-formed",
  "arguments": {
    "statements": [
      "all x (man(x) -> mortal(x))",
      "man(socrates)"
    ]
  }
}

文档

参见Documents文件夹以获取详细的分析和示例：

• 知识到应用：对AI系统中理解和实际应用的正式逻辑分析

项目结构

mcp-logic/
├── src/
│   └── mcp_logic/
│       └── server.py   # Main MCP server implementation
├── tests/
│   ├── test_proofs.py  # Core functionality tests
│   └── test_debug.py   # Debug utilities
├── Documents/          # Analysis and documentation
├── pyproject.toml      # Python package config
├── setup-script.sh     # Setup script (installs LADR & dependencies)
├── run-mcp-logic.sh    # Docker-based run script (Linux/macOS)
├── run-mcp-logic.bat   # Docker-based run script (Windows)
├── run-mcp-logic-local.sh # Local run script (no Docker)
└── README.md           # This file

注意：运行setup-script.sh后，会创建一个包含Prover9二进制文件的"ladr"目录，但该目录并未包含在仓库本身中。

开发

运行测试：

uv pip install pytest
uv run pytest

许可证

MIT