🚀 MCP 服务器逻辑求解器
MCP 服务器逻辑求解器是一款强大的工具，专注于处理一阶逻辑问题。它巧妙融合自然语言理解与形式化逻辑推理，能对给定前提和结论进行验证，并给出“True”“False”或“Uncertain”的结果。
🚀 快速开始
MCP 服务器逻辑求解器可对一阶逻辑问题进行有效验证。在使用前，需确保输入遵循特定格式规范，同时完成服务器的安装、配置等准备工作。
✨ 主要特性
- 智能验证：结合自然语言理解和形式化逻辑推理，对前提和结论进行验证。
- 多语言支持：解析器支持中文和英文，方便不同语言背景的用户使用。
- 灵活输出：输出布尔结果（True/False/Uncertain）及详细解释，便于用户理解推理过程。
📦 安装指南
先决条件
- 安装 MCP-Logic 服务器
- 下载并编译源代码。
- 配置运行环境变量。
- 配置 API 接口
- 设置 API 访问密钥。
- 调试连接测试。
- 准备输入数据
- 确保格式正确性。
- 进行语法和语义检查。
环境变量配置
创建一个 .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 服务器需要遵循以下格式规范：
- 前提与结论：
- 自然语言形式：用简洁明了的中文描述。
- 一阶逻辑形式：使用标准的符号和术语，如∀、∃、¬、∧、∨等。
- 符号转换规则：
- ∀ → 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 服务器逻辑求解器来解决各种复杂的问题。