AI导哈

逻辑求解器

一个结合大型语言模型（LLMs）和形式化定理证明能力的强大逻辑推理系统，用于自动推理和逻辑验证。

  • by RyanNg1403
  • Python
  • 本地部署
  • 1 星标
  • 更新于
在 GitHub 查看 ryanng1403/mcp-server-logical-solver

使用说明

MCP服务器逻辑求解器

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

概述

该系统旨在：

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

FOL输入要求

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

  1. 逻辑运算符：

    • 通用量词：∀（翻译为“所有”）
    • 存在量词：∃（翻译为“存在”）
    • 连词：∧（翻译为“&”）
    • 分离：∨（翻译为“|”）
    • 含义：→ （翻译为“->”）
    • 双重含义：↔ （翻译为“<->”）
    • 否定：¬（翻译为“-”）
    • 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)

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

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找不到证明。这一结果需要进一步分析，因为它可能意味着：

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

该系统使用基于LLM的分析来区分“假”和“不确定”情况 SEARCH FAILED 遇到。

先决条件

在设置此项目之前，您需要：

  1. 设置MCP逻辑服务器：

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

  2. 遵循MCP逻辑设置说明：

    • 对于Windows：
      windows-setup-mcp-logic.bat
    • 对于Linux：
      chmod +x linux-setup-script.sh
./linux-setup-script.sh

  3. 启动MCP逻辑服务器：

    • 对于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逻辑 .

运行项目

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逻辑服务器是否正在运行
    • 检查中的端口设置 mcp_config.json
    • 确保没有防火墙阻止连接

  2. 模型API问题

    • 在中验证您的API密钥 .env 文件
    • 检查您是否有足够的API信用
    • 确保所选型号适用于您的帐户

  3. 输入格式问题

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

相关 MCP