一个用于使用 Prover9 和 Mace4 进行自动一阶逻辑推理的 MCP 服务器。
定理证明 - 使用 Prover9 证明逻辑陈述
模型查找 - 使用 Mace4 查找有限模型
反例查找 - 展示陈述为何不成立
语法验证 - 通过有用的错误消息预先验证公式
范畴推理 - 内置对范畴论证明的支持
命题偶然性 - 用于快速命题检查的纯分析性 HCC 证明器
溯因推理 - 使用变分自由能 (VFE) 对假设进行排序
自包含 - 所有依赖项自动安装
Related MCP server: warrant-mcp
Linux/macOS:
git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
./linux-setup-script.shWindows:
git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
windows-setup-mcp-logic.bat安装脚本会自动：
下载并构建 LADR (Prover9 + Mace4)
创建 Python 虚拟环境
安装所有依赖项
生成 Claude Desktop 配置
添加到您的 Claude Desktop MCP 配置中（在 claude-app-config.json 中自动生成）：
{
"mcpServers": {
"mcp-logic": {
"command": "uv",
"args": [
"--directory",
"/absolute/path/to/mcp-logic/src/mcp_logic",
"run",
"mcp_logic",
"--prover-path",
"/absolute/path/to/mcp-logic/ladr/bin"
]
}
}
}重要提示： 请将 /absolute/path/to/mcp-logic 替换为您实际的仓库路径。
工具 | 用途 |
prove | 使用 Prover9 证明陈述 |
check-well-formed | 验证公式语法并提供详细错误信息 |
find_model | 查找满足前提的有限模型 |
find_counterexample | 查找证明陈述不成立的反例 |
verify_commutativity | 为范畴图交换性生成 FOL |
get_category_axioms | 获取范畴/函子/群/幺半群的公理 |
check_contingency | 通过 HCC 证明器检查真值函数偶然性 |
abductive_explain | 为观察结果查找最小化 VFE 的解释 |
Use the mcp-logic prove tool with:
premises: ["all x (man(x) -> mortal(x))", "man(socrates)"]
conclusion: "mortal(socrates)"结果： ✓ 定理已证明
Use the mcp-logic check_contingency tool with:
formula: "(p -> q) | (q -> p)"结果： 识别出该公式为非偶然的重言式，并返回证明轨迹。
Use the mcp-logic find-counterexample tool with:
premises: ["P(a)"]
conclusion: "P(b)"结果： 找到一个模型，其中 P(a) 为真但 P(b) 为假，证明结论不成立。
Use the mcp-logic verify-commutativity tool with:
path_a: ["f", "g"]
path_b: ["h"]
object_start: "A"
object_end: "C"结果： 用于证明 f∘g = h 的 FOL 前提和结论。
不使用 Claude Desktop，直接运行服务器：
Linux/macOS:
./run_mcp_logic.shWindows:
run_mcp_logic.batmcp-logic/
├── src/mcp_logic/
│ ├── server.py # Main MCP server (8 tools)
│ ├── mace4_wrapper.py # Mace4 model finder
│ ├── syntax_validator.py # Formula syntax validation
│ ├── categorical_helpers.py # Category theory utilities
│ ├── hcc_prover.py # Hypersequent Contingency Calculus prover
│ ├── vfe_engine.py # Variational Free Energy abductive engine
│ └── formula_ast.py # Propositional logic AST and parser
├── ladr/ # Auto-installed Prover9/Mace4 binaries
│ └── bin/
│ ├── prover9
│ └── mace4
├── tests/ # Test suite
├── linux-setup-script.sh # Linux/macOS setup
├── windows-setup-mcp-logic.bat # Windows setup
├── run_mcp_logic.sh # Linux/macOS run script
└── run_mcp_logic.bat # Windows run script认知架构增强：
✅ 超序列偶然性演算 (HCC)： 增加了一个严谨的演绎检查器，无需暴力建模即可即时评估命题公式的偶然性。
✅ 变分自由能 (VFE) 引擎： 实现了溯因推理，使用非教条的 Cournot-Gaifman 先验对假设进行排序，以优雅地满足奥卡姆剃刀原则。
✅ 智能证明器路由： prove 工具会自动将纯命题查询路由到 HCC 引擎，将一阶查询路由到 Prover9。
✅ 可配置模型查找器： find_model 和 find_counterexample 现在支持自定义超时和结构化谓词/函数提取。
增强功能：
✅ Mace4 模型查找和反例检测
✅ 带有位置特定错误的详细语法验证
✅ 范畴推理支持（范畴论公理、交换性验证）
✅ 所有工具的结构化 JSON 输出
✅ 自包含安装（无需手动路径配置）
运行测试：
source .venv/bin/activate
pytest tests/ -v直接测试组件：
python tests/test_enhancements.pyENHANCEMENTS.md - v0.2.0 功能快速参考
Documents/ - 详细分析和示例
walkthrough.md - 实现细节（在工件中）
“Prover9 not found” 错误：
运行安装脚本：./linux-setup-script.sh 或 windows-setup-mcp-logic.bat
检查 ladr/bin/prover9 和 ladr/bin/mace4 是否存在
服务器未更新：
代码更改后重启服务器
检查日志中的语法错误
语法验证警告：
谓词/函数请使用小写（例如 man(x) 而不是 Man(x)）
在运算符周围添加空格以提高清晰度
确保所有括号匹配
This server cannot be installed
Unclaimed servers have limited discoverability.
If you are the server author, to access and configure the admin panel.
MCP server for AI agents to plan, verify, and deploy Cloudflare-native apps.
MCP server for AI dialogue using various LLM models via AceDataCloud
An MCP server that integrates with Discord to provide AI-powered features.
We provide all the information about MCP servers via our MCP API.
curl -X GET 'https://glama.ai/api/mcp/v1/servers/angrysky56/mcp-logic'
If you have feedback or need assistance with the MCP directory API, please join our Discord server