🚀 MCP-Logic 服务器
MCP-Logic 服务器是一个提供自动化推理能力的MCP服务器，借助 Prover9/Mace4 为 AI 系统赋予逻辑推理功能。它通过简洁的 MCP 接口，实现定理证明和逻辑模型验证，极大地提升了 AI 系统在逻辑推理方面的效率和准确性。
🚀 快速开始
MCP-Logic 通过专门针对 AI 系统的接口设计，填补了 AI 与形式逻辑之间的鸿沟。以下是一个快速示例，展示如何使用 MCP-Logic 进行逻辑推理：
# 证明理解加上上下文能够应用于实际
if __name__ == "__main__":
knowledge = [
"所有人类都是有生命的生物。", # 前提1：man(x) → mortal(x)
"苏格拉底是人。" # 前提2：man(socrates)
]
conclusion = "苏格拉底是有生命的。"
run_knowledge_to_application(knowledge, conclusion)
输出结果
所有人类都是有生命的生物。 # 前提1：man(x) → mortal(x)
苏格拉底是人。 # 前提2：man(socrates)
结论：苏格拉底是有生命的。 # 结论：mortal(socrates)
证明过程：
1. 根据前提1，人类的定义决定了所有人类都是有生命的。
2. 前提2指出苏格拉底属于人类范畴。
3. 因此，通过逻辑推理得出苏格拉底是有生命的结论。
✨ 主要特性
- AI优先设计：专为 AI 系统打造，支持自动化推理，让 AI 系统能够更高效地进行逻辑推理。
- 知识验证：能够对知识表示及其逻辑推论进行正式验证，确保知识的准确性和可靠性。
- 无缝集成：与模型上下文协议（MCP）生态系统完美兼容，方便与其他系统进行集成。
- 深度推理：支持复杂逻辑证明，包括嵌套量词和多前提推理，满足各种复杂场景的需求。
- 实际应用：特别适用于 AI 知识模型和推理链的验证，为 AI 系统的实际应用提供有力支持。
- 与 Prover9 无缝集成，支持定理自动证明，提高证明效率。
- 支持复杂的逻辑公式和证明，处理各种复杂的逻辑问题。
- 内置语法验证功能，确保输入的逻辑公式符合语法规则。
- 搭配有 MCP 协议的干净服务器接口，提供简洁易用的接口。
- 具备完善的错误处理和日志记录，方便调试和维护。
- 支持知识表示及 AI 系统的推理分析，助力 AI 系统的开发和优化。
📦 安装指南
系统要求
- 操作系统：Linux/macOS/Windows
- 内存：建议至少 4GB RAM
- 磁盘空间：至少 10GB 可用空间
安装步骤
# 下载项目源码
git clone https://github.com/yourusername/mcp-logic.git
cd mcp-logic
# 运行设置脚本（根据系统选择对应脚本）
# 对于Linux/macOS：
./setup-script.sh
# 对于Windows：
./setup-script.bat
# 安装完成后，生成ladr目录包含Prover9二进制文件
💻 使用示例
基础用法
1. 定理证明工具
{
"tool": "prove-theorem",
"arguments": {
"premises": [
"所有人类都是有生命的生物。",
"苏格拉底是人。"
],
"conclusion": "苏格拉底是有生命的。"
}
}
2. 语法验证工具
{
"tool": "check-well-formed",
"arguments": {
"statements": [
"所有人类都是有生命的生物。",
"苏格拉底是人。"
]
}
}
📚 详细文档
查看Documents文件夹中的详细分析和示例：
- 知识到应用：关于理解与实际应用在 AI 系统中的形式逻辑分析
🔧 技术细节
项目结构
mcp-logic/
├── src/
│ └── mcp_logic/
│ └── server.py # 主MCP服务器实现文件
├── tests/
│ ├── test_proofs.py # 核心功能测试用例
│ └── test_debug.py # 调试工具测试
├── Documents/ # 分析与文档资料
├── pyproject.toml # Python包配置文件
├── setup-script.sh # 设置脚本（安装LADR及依赖）
├── run-mcp-logic.sh # 基于Docker运行脚本（Linux/macOS）
├── run-mcp-logic.bat # 基于Docker运行脚本（Windows）
├── run-mcp-logic-local.sh # 本地运行脚本（无Docker）
└── README.md # 该项目说明文档
注：运行设置脚本后，会在项目目录下生成一个ladr文件夹，其中包含 Prover9 二进制文件，但该文件夹不会被纳入仓库版本控制。
开发指南
运行测试用例
uv pip install pytest
uv run pytest
📄 许可证
本项目采用 MIT 许可证。