MCP Server Logical Solver

MCP Server Logical Solver

一款功能强大的逻辑推理系统，将大语言模型（LLM）与形式化定理证明能力相结合。本项目利用 MCP-Logic 服务提供自动推理和逻辑验证。

概述

此系统旨在：

• 处理自然语言和一阶逻辑（FOL）格式的逻辑问题
• 通过 Prover9/Mace4 使用自动定理证明
• 使用基于 LLM 的分析提供结构化推理
• 处理包括 XOR 转换在内的复杂逻辑运算
• 为逻辑结论生成详细解释

FOL 输入要求

一阶逻辑（FOL）输入必须严格遵循 Prover9 的语法要求：

1. 逻辑运算符：

   • 全称量词：∀（转换为 'all'）
   • 存在量词：∃（转换为 'exists'）
   • 合取：∧（转换为 '&'）
   • 析取：∨（转换为 '|'）
   • 蕴含：→（转换为 '->'）
   • 双向蕴含：↔（转换为 '<->'）
   • 否定：¬（转换为 '-'）
   • XOR 运算：⊕（自动转换为等价形式）

2. 格式指南：

   • 前提和结论必须是格式良好的公式
   • 变量和谓词应遵循 Prover9 的命名约定
   • XOR 表达式会自动转换为使用否定和双向蕴含的等价形式

示例：

# Original FOL with Unicode
∀x (P(x) ∧ Q(x)) → (R(x) ⊕ S(x))

# Translated for Prover9
all x ((P(x) & Q(x)) -> -(R(x) <-> S(x)))

核心组件

1. 逻辑求解器（main.py）

• 通过两阶段流程处理逻辑问题：
  • 第一阶段：使用集成 Prover9 的 LLM 进行详细逻辑分析
  • 第二阶段：对推理过程进行结构化总结
• 支持批量处理多个逻辑问题
• 提供全面的输出，包括前提、结论和解释

2. 模板（template.py）

• LOGICAL_SOLVER_TEMPLATE：指导 LLM 求解逻辑问题
  • 结合自然语言和 FOL 分析
  • 集成 Prover9 进行形式化验证
  • 提供结构化推理指南
• LOGICAL_SUMMARIZER_TEMPLATE：确保输出格式一致
  • 生成 JSON 结构化响应
  • 包含解释、答案和工具使用信息

3. 解析器（parser.py）

• 处理 FOL 公式转换
• 专门处理 XOR 运算
• 确保与 Prover9 语法兼容

4. Prover9 输出解读

系统对 Prover9 的定理证明结果作如下解读：

• THEOREM PROVED：表示 Prover9 已找到正式证明，表明结论可由前提逻辑推出。此时系统返回“True”。

• SEARCH FAILED：表示 Prover9 未能找到证明。此结果需要进一步分析，因为它可能意味着：

  • “False”：前提明显与结论矛盾或不支持结论时
  • “Uncertain”：前提不足以确定结论的真值时

遇到 SEARCH FAILED 时，系统会使用基于 LLM 的分析来区分“False”和“Uncertain”情况。

先决条件

设置此项目之前，你需要：

1. 设置 MCP-Logic 服务：

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

2. 按照 MCP-Logic 设置说明操作：

   • Windows：

     windows-setup-mcp-logic.bat
     

   • Linux：

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

3. 启动 MCP-Logic 服务：

   • Windows：

     run-mcp-logic.bat
     

   • Linux：

     ./run-mcp-logic.sh
     

安装

1. 克隆此仓库：

   git clone [your-repository-url]
   cd mcp-server-logical-solver
   

2. 安装依赖：

   pip install -r requirements.txt
   

配置

1. 环境变量（.env）

在根目录中创建 .env 文件，并进行以下设置：

# Model Configuration
MODEL_PROVIDER=openai  # Options: openai, anthropic, gemini, ollama
MODEL_NAME=gpt-4  # Specify your model name
API_KEY=your_api_key_here  # Required for OpenAI/Anthropic/Gemini

# Optional Settings
DEBUG=False  # Enable debug mode

2. MCP 配置 (mcp_config.json)

将根目录中的 mcp_config_example.json 改为 mcp_config.json：

{
  "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"
      ]
    }
  }
}

请务必调整 --prover-path 和 --directory 的值，使其与克隆 MCP-Logic 的位置相匹配。

运行项目

1. 基本用法（单个问题）

python test.py

这将处理一个示例问题，并将输出保存到 output.json。

2. 批量处理

python main.py input.json output.json

其中：

• input.json：包含逻辑问题的输入文件路径
• output.json：保存结果的路径

输入 JSON 格式：

[
  {
    "premises": "Natural language premises...",
    "premises-FOL": "First order logic premises...",
    "conclusion": "Natural language conclusion...",
    "conclusion-FOL": "First order logic conclusion...",
    "label": "True/False/Uncertain"  // Optional ground truth
  }
]

输出格式

系统会生成以下格式的结构化输出。tool_use 表示工具调用是否成功：

{
    "premises": "Original natural language premises",
    "premises-FOL": "Processed FOL premises",
    "conclusion": "Natural language conclusion",
    "conclusion-FOL": "FOL conclusion",
    "answer": "True/False/Uncertain",
    "explanation": "Detailed reasoning process",
    "tool_use": "True/False"
}

故障排查

1. MCP 服务连接问题

   • 确认 MCP-Logic 服务正在运行
   • 检查 mcp_config.json 中的端口设置
   • 确保防火墙未阻止连接

2. 模型 API 问题

   • 确认 .env 文件中的 API 密钥
   • 检查 API 额度是否充足
   • 确保所选模型可供你的账户使用

3. 输入格式问题

   • 验证输入 JSON 格式
   • 确保 FOL 语句格式正确
   • 检查逻辑符号中是否使用了正确的 Unicode 字符