MCP-Logic

基本能力

产品定位

MCP-Logic 旨在为 AI 系统提供自动推理能力，通过逻辑定理证明和模型验证，帮助验证知识表示和逻辑推理的正确性。

核心功能

• 自动定理证明：集成 Prover9 进行逻辑定理证明。
• 复杂逻辑支持：支持复杂逻辑公式和证明，包括嵌套量词和多前提。
• 语法验证：内置语法验证功能。
• MCP 接口：提供简洁的 MCP 服务器接口。
• 错误处理与日志：完善的错误处理和日志功能。
• 知识表示与推理：支持 AI 系统的知识表示和推理。

适用场景

• AI 知识模型验证：验证 AI 系统的知识表示和逻辑推理链。
• 逻辑推理研究：用于逻辑推理和定理证明的研究。
• 教育工具：作为逻辑学和 AI 教育的辅助工具。

工具列表

• prove：运行逻辑证明的工具。
• check-well-formed：验证逻辑语句语法的工具。

常见问题解答

• 依赖安装：确保安装 Python 3.12+ 和 UV 包管理器。
• Prover9/Mace4 安装：需从指定链接下载并安装到指定路径。

使用教程

使用依赖

1. 安装 Python 3.12+。
2. 安装 UV 包管理器。
3. 下载 Prover9/Mace4 并安装到指定路径（如 F:/Prover9-Mace4/）。

安装教程

1. 克隆仓库。
2. 安装依赖：

uv venv
uv pip install -e .

1. 配置 MCP 环境：

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

调试方式

运行测试：

uv pip install pytest
uv run pytest

许可证

该项目遵循 MIT 开源许可条款，请参阅 MIT 了解完整条款。