MCP Server Logical Solver

🚀 MCP 服务器逻辑求解器

MCP 服务器逻辑求解器是一款强大的工具，专注于处理一阶逻辑问题。它巧妙融合自然语言理解与形式化逻辑推理，能对给定前提和结论进行验证，并给出“True”“False”或“Uncertain”的结果。

🚀 快速开始

MCP 服务器逻辑求解器可对一阶逻辑问题进行有效验证。在使用前，需确保输入遵循特定格式规范，同时完成服务器的安装、配置等准备工作。

✨ 主要特性

• 智能验证：结合自然语言理解和形式化逻辑推理，对前提和结论进行验证。
• 多语言支持：解析器支持中文和英文，方便不同语言背景的用户使用。
• 灵活输出：输出布尔结果（True/False/Uncertain）及详细解释，便于用户理解推理过程。

📦 安装指南

先决条件

1. 安装 MCP-Logic 服务器
   • 下载并编译源代码。
   • 配置运行环境变量。
2. 配置 API 接口
   • 设置 API 访问密钥。
   • 调试连接测试。
3. 准备输入数据
   • 确保格式正确性。
   • 进行语法和语义检查。

环境变量配置

创建一个 .env 文件，内容如下：

DEBUG=False
API_KEY=your_api_key_here

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

💻 使用示例

基础用法

[
  {
    "前提": "所有人类都是会死的",
    "前提-FOL": "∀x（Human(x) → Mortal(x))",
    "结论": "苏格拉底是人类，因此他会死",
    "结论-FOL": "Human(Socrates) ∧ Mortal(Socrates)"
  }
]

将上述输入保存为 input.json，然后在终端中执行：

python main.py input.json output.json

输出结果将保存为 output.json。

高级用法

当需要批量处理多个一阶逻辑问题时，可在 input.json 中添加多个对象，每个对象代表一个问题，然后执行批量处理命令：

python main.py input.json output.json

📚 详细文档

一阶逻辑输入要求

为了确保输入的一致性和正确性，MCP 服务器需要遵循以下格式规范：

1. 前提与结论：
   • 自然语言形式：用简洁明了的中文描述。
   • 一阶逻辑形式：使用标准的符号和术语，如∀、∃、¬、∧、∨等。
2. 符号转换规则：
   • ∀ → all
   • ∃ → exists
   • ¬ → not
   • ∧ → and
   • ∨ → or

关键组件

1. 逻辑求解器（Logical Solver）

• 功能：负责解析和验证一阶逻辑表达式。
• 输入：自然语言描述和对应的一阶逻辑表达式。
• 输出：布尔结果（True/False/Uncertain）及详细解释。

2. 模板文件（Templates）

• 作用：定义接口规范和交互协议。
• 内容：
  • 输入数据格式
  • 输出数据结构
  • 错误处理机制

3. 解析器（Parser）

• 功能：将自然语言转换为一阶逻辑表达式。
• 支持的语言：中文、英文。

输出格式

生成的输出文件将包含以下字段：

{
    "前提": "原始自然语言描述",
    "前提-FOL": "处理后的一阶逻辑表达式",
    "结论": "目标结论",
    "结论-FOL": "对应的一阶逻辑形式",
    "答案": "True/False/Uncertain",
    "解释": "详细推理过程",
    "工具调用": "True/False"
}

🔧 技术细节

MCP 服务器逻辑求解器主要由逻辑求解器、模板文件和解析器三个关键组件构成。逻辑求解器负责核心的逻辑表达式解析和验证工作，模板文件定义了接口规范和交互协议，解析器则实现了自然语言到一阶逻辑表达式的转换。通过这些组件的协同工作，求解器能够高效地处理一阶逻辑问题。

📄 故障排除

1. MCP 服务器连接问题

• 确认服务器正在运行。
• 检查端口配置是否正确。
• 查看网络连接状态。

2. 输入数据错误

• 核对格式规范。
• 进行语法检查。
• 确保内容一致性。

通过以上步骤，您可以高效地使用 MCP 服务器逻辑求解器来解决各种复杂的问题。