MCP-Logic 使用说明

项目简介

MCP-Logic 是一个基于 Model Context Protocol (MCP) 构建的服务器，旨在为人工智能系统提供强大的自动逻辑推理能力。它集成了 Prover9 和 Mace4 这两个著名的定理证明器和模型检验器，通过简洁的 MCP 接口，使得 AI 应用能够方便地进行知识验证、逻辑推理和形式化分析。

主要功能点

逻辑定理证明: 使用 Prover9 自动证明逻辑定理，验证知识表示的有效性和逻辑推导的正确性。
逻辑模型检验: 利用 Mace4 进行逻辑模型检验（仓库中未明确提及，但 Prover9/Mace4 套件通常包含此功能，可能在未来扩展）。
语法验证: 检查逻辑语句的语法是否正确，帮助用户确保输入的逻辑表达式符合规范。
MCP 协议接口: 完全兼容 Model Context Protocol，可以无缝集成到任何支持 MCP 协议的 AI 客户端。
工具化调用: 通过 'prove' 和 'check-well-formed' 等工具，以标准化的方式向 LLM 提供逻辑推理和验证能力。

安装步骤

安装 Python 3.12+ 和 UV 包管理器: 确保你的系统已安装 Python 3.12 或更高版本，并安装了 UV 包管理器。
下载 Prover9/Mace4: 访问 Prover9/Mace4 下载页面，根据你的操作系统下载并解压 Prover9/Mace4 软件包。

克隆仓库: 使用 Git 克隆 MCP-Logic 仓库到本地：

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

安装 Python 依赖: 在仓库根目录下，使用 UV 创建虚拟环境并安装项目依赖：
```
uv venv
uv pip install -e .
```

服务器配置

要将 MCP-Logic 服务器配置到 MCP 客户端，你需要在客户端的 MCP 服务器配置中添加以下 JSON 信息。请根据你的实际 Prover9/Mace4 安装路径和 MCP-Logic 仓库路径进行修改。

{
  "mcpServers": {
    "mcp-logic": {
      "command": "uv",
      "args": [
        "--directory",
        "path/to/mcp-logic/src/mcp_logic",  //  指向 mcp_logic 服务器代码所在的目录
        "run",
        "mcp_logic",                      //  运行 mcp_logic 服务器程序
        "--prover-path",
        "path/to/Prover9-Mace4/bin-win32"   //  Prover9/Mace4  可执行文件所在的目录，例如 "F:/Prover9-Mace4/bin-win32"
      ]
    }
  }
}

配置参数说明:

'command': 启动服务器的命令，这里使用 'uv run' 来运行 Python 程序。
'args': 传递给 'uv run' 命令的参数列表。
- '--directory "path/to/mcp-logic/src/mcp_logic"': 指定 UV 运行的工作目录为 'mcp_logic' 目录，这是服务器代码所在的位置。请替换 '"path/to/mcp-logic"' 为你本地仓库的实际路径。
- 'run': UV 的子命令，用于运行 Python 包或模块。
- 'mcp_logic': 要运行的 Python 模块名，对应 'src/mcp_logic/main.py' 或 'src/mcp_logic/server.py'。
- '--prover-path "path/to/Prover9-Mace4/bin-win32"': MCP-Logic 服务器特有的参数，用于指定 Prover9/Mace4 可执行文件的路径。请替换 '"path/to/Prover9-Mace4/bin-win32"' 为你本地 Prover9/Mace4 的实际安装路径。

基本使用方法

配置完成后，MCP 客户端就可以调用 MCP-Logic 服务器提供的工具。以下是 'prove' 和 'check-well-formed' 两个工具的基本使用示例。

1. 使用 'prove' 工具进行逻辑定理证明:

发送如下 JSON-RPC 请求给 MCP 服务器，调用 'prove' 工具：

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

服务器会返回证明结果，例如：

{
  "result": "proved",
  "proof": "...",
  "complete_output": "..."
}

2. 使用 'check-well-formed' 工具进行语法验证:

发送如下 JSON-RPC 请求给 MCP 服务器，调用 'check-well-formed' 工具：

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

服务器会返回语法检查结果，指示语句是否有效，以及详细信息：

{
  "valid": false,
  "details": {
    "result": "error",
    "reason": "Syntax error",
    "error": "..."
  }
}

请参考仓库文档和测试用例，了解更多高级用法和工具参数。

关键词