MCP逻辑
一个使用 Prover9/Mace4 为人工智能系统提供自动推理功能的 MCP 服务器。该服务器通过简洁的 MCP 接口实现逻辑定理证明和逻辑模型验证。
设计理念
MCP-Logic 通过提供与 Prover9/Mace4 的强大接口，弥合了 AI 系统与形式逻辑之间的差距。它的独特之处：
- AI-First 设计：专为执行自动推理的 AI 系统构建
- 知识验证：实现知识表示和逻辑含义的形式化验证
- 清洁集成：与模型上下文协议（MCP）生态系统无缝集成
- 深度推理：支持嵌套量词和多重前提的复杂逻辑证明
- 现实世界的应用：对于验证人工智能知识模型和推理链特别有用
特征
- 与 Prover9 无缝集成，实现自动定理证明
- 支持复杂的逻辑公式和证明
- 内置语法验证
- 清理 MCP 服务器界面
- 广泛的错误处理和日志记录
- 支持人工智能系统的知识表示和推理
快速示例
# Prove that understanding + context leads to application
result = await prove(
premises=[
"all x all y (understands(x,y) -> can_explain(x,y))",
"all x all y (can_explain(x,y) -> knows(x,y))",
"all x all y (knows(x,y) -> believes(x,y))",
"all x all y (believes(x,y) -> can_reason_about(x,y))",
"all x all y (can_reason_about(x,y) & knows_context(x,y) -> can_apply(x,y))",
"understands(system,domain)",
"knows_context(system,domain)"
],
conclusion="can_apply(system,domain)"
)
# Returns successful proof!
安装
先决条件
- Python 3.10+
- UV包管理器
- Git 用于克隆存储库
- CMake 和构建工具（用于构建 LADR/Prover9）
设置
克隆此存储库
git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
运行安装脚本：Windows 运行：
windows-setup-mcp-logic.bat
Linux/macOS：
chmod +x linux-setup-script.sh
./linux-setup-script.sh
安装脚本：
- 检查依赖项（git、cmake、构建工具）
- 从外部存储库下载 LADR（Prover9/Mace4）： laitep/LADR
- 构建 LADR 库以在 ladr/bin 目录中创建 Prover9 二进制文件
- 创建 Python 虚拟环境
- 设置使用或不使用 Docker 运行的配置文件
重要提示：LADR 目录不包含在存储库本身中，将通过安装脚本或手动安装。
使用 Docker-不知道这是否正常工作，主要设计用于直接与 Claude Desktop 一起使用
如果您更喜欢使用 Docker 运行此脚本：
- 找到可用端口
- 激活虚拟环境
- 使用安装的 Prover9 的正确路径运行服务器
# Linux/macOS
./run-mcp-logic.sh
# Windows
run-mcp-logic.bat
这些脚本将构建并运行具有必要环境的 Docker 容器。
Claude 桌面集成
要将 MCP-Logic 与 Claude Desktop 一起使用，请使用以下配置：
{
"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"
]
}
}
}
用您的实际存储库路径替换“/path/to/mcp-logic”。
可用工具
证明
使用 Prover9 运行逻辑证明：
{
"tool": "prove",
"arguments": {
"premises": [
"all x (man(x) -> mortal(x))",
"man(socrates)"
],
"conclusion": "mortal(socrates)"
}
}
检查格式是否正确
验证逻辑语句语法：
{
"tool": "check-well-formed",
"arguments": {
"statements": [
"all x (man(x) -> mortal(x))",
"man(socrates)"
]
}
}
文档
详细分析和示例请参阅文档文件夹：
项目结构
mcp-logic/
├── src/
│ └── mcp_logic/
│ └── server.py # Main MCP server implementation
├── tests/
│ ├── test_proofs.py # Core functionality tests
│ └── test_debug.py # Debug utilities
├── Documents/ # Analysis and documentation
├── pyproject.toml # Python package config
├── setup-script.sh # Setup script (installs LADR & dependencies)
├── run-mcp-logic.sh # Docker-based run script (Linux/macOS)
├── run-mcp-logic.bat # Docker-based run script (Windows)
├── run-mcp-logic-local.sh # Local run script (no Docker)
└── README.md # This file
注意：运行 setup-script.sh 后，将创建一个包含 Prover9 二进制文件的“ladr”目录，但该目录不包含在存储库本身中。
发展
运行测试：
uv pip install pytest
uv run pytest
执照
麻省理工学院