MCP-Logic

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

设计理念

MCP-Logic通过提供与Prover9/Mace4的强大接口，弥合了AI系统与形式逻辑之间的差距。其独特之处在于：

• 面向AI的设计：专门为AI系统设计，以执行自动推理
• 知识验证：能够对知识表示和逻辑推论进行正式验证
• 无缝集成：与模型上下文协议（MCP）生态系统无缝集成
• 深度推理：支持带有嵌套量词和多个前提的复杂逻辑证明
• 实际应用：特别适用于验证AI知识模型和推理链

特性

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

快速示例

# 证明理解+上下文导致应用
result = await prove(
    前提条件=[
        "所有 x 所有 y (理解(x,y) -> 能解释(x,y))",
        "所有 x 所有 y (能解释(x,y) -> 知道(x,y))",
        "所有 x 所有 y (知道(x,y) -> 相信(x,y))",
        "所有 x 所有 y (相信(x,y) -> 能推理(x,y))",
        "所有 x 所有 y (能推理(x,y) & 知道上下文(x,y) -> 能应用(x,y))",
        "理解(系统,领域)",
        "知道上下文(系统,领域)"
    ],
    结论="能应用(系统,领域)"
)
# 返回成功的证明！

安装

先决条件

• 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": {
      "命令": "uv",
      "参数": [
        "--目录", 
        "/path/to/mcp-logic/src/mcp_logic",
        "运行", 
        "mcp_logic", 
        "--prover-path", 
        "/path/to/mcp-logic/ladr/bin"
      ]
    }
  }
}

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

可用工具

prove

使用Prover9运行逻辑证明：

{
  "工具": "prove",
  "参数": {
    "前提条件": [
      "所有 x (人(x) -> 凡人(x))",
      "人(苏格拉底)"
    ],
    "结论": "凡人(苏格拉底)"
  }
}

check-well-formed

验证逻辑语句语法：

{
  "工具": "check-well-formed",
  "参数": {
    "语句": [
      "所有 x (人(x) -> 凡人(x))",
      "人(苏格拉底)"
    ]
  }
}

文档

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

• 知识到应用：关于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           # 此文件

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

开发

运行测试：

uv pip install pytest
uv run pytest

许可证

MIT