MCP-Logic

一个 MCP 服务器，为 AI 系统提供使用 Prover9/Mace4 的自动推理能力。该服务器通过一个清晰的 MCP 接口实现逻辑定理证明和逻辑模型验证。

设计理念

MCP-Logic 通过提供一个到 Prover9/Mace4 的强大接口，弥合了 AI 系统和形式逻辑之间的差距。它的特别之处在于：

• AI 优先设计：专为 AI 系统执行自动推理而构建
• 知识验证：支持对知识表示和逻辑蕴涵进行形式验证
• 清洁集成：与模型上下文协议 (MCP) 生态系统无缝集成
• 深度推理：支持具有嵌套量词和多个前提的复杂逻辑证明
• 实际应用：特别适用于验证 AI 知识模型和推理链

特性

• 与 Prover9 无缝集成，实现自动定理证明
• 支持复杂的逻辑公式和证明
• 内置语法验证
• 清晰的 MCP 服务器接口
• 广泛的错误处理和日志记录
• 支持知识表示和关于 AI 系统的推理

快速示例

# 证明理解 + 上下文导致应用
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)"
)
# 返回成功的证明！

{'result': 'proved', 'proof': '', 'complete_output': '============================== Prover9 ===============================\nProver9 (32) version Dec-2007, Dec 2007.\nProcess 27928 was started by angry on Ty,\nMon Jan 13 16:10:57 2025\nThe command was "/cygdrive/f/Prover9-Mace4/bin-win32/prover9 -f C:\Users\angry\AppData\Local\Temp\tmp05_k_2ak.in".\n============================== end of head ===========================\n\n============================== INPUT =================================\n\n% Reading from file C:\Users\angry\AppData\Local\Temp\tmp05_k_2ak.in\n\n\nformulas(assumptions).\n(all x all y (understands(x,y) -> can_explain(x,y))).\n(all x all y (can_explain(x,y) -> knows(x,y))).\n(all x all y (knows(x,y) -> believes(x,y))).\n(all x all y (believes(x,y) -> can_reason_about(x,y))).\n(all x all y (can_reason_about(x,y) & knows_context(x,y) -> can_apply(x,y))).\nunderstands(system,domain).\nknows_context(system,domain).\nend_of_list.\n\nformulas(goals).\ncan_apply(system,domain).\nend_of_list.\n\n============================== end of input ==========================\n\n============================== PROCESS NON-CLAUSAL FORMULAS ==========\n\n% Formulas that are not ordinary clauses:\n1 (all x all y (understands(x,y) -> can_explain(x,y))) # label(non_clause). [assumption].\n2 (all x all y (can_explain(x,y) -> knows(x,y))) # label(non_clause). [assumption].\n3 (all x all y (knows(x,y) -> believes(x,y))) # label(non_clause). [assumption].\n4 (all x all y (believes(x,y) -> can_reason_about(x,y))) # label(non_clause). [assumption].\n5 (all x all y (can_reason_about(x,y) & knows_context(x,y) -> can_apply(x,y))) # label(non_clause). [assumption].\n6 can_apply(system,domain) # label(non_clause) # label(goal). [goal].\n\n============================== end of process non-clausal formulas ===\n\n============================== PROCESS INITIAL CLAUSES ===============\n\n% Clauses before input processing:\n\nformulas(usable).\nend_of_list.\n\nformulas(sos).\n-understands(x,y) | can_explain(x,y). [clausify(1)].\n-can_explain(x,y) | knows(x,y). [clausify(2)].\n-knows(x,y) | believes(x,y). [clausify(3)].\n-believes(x,y) | can_reason_about(x,y). [clausify(4)].\n-can_reason_about(x,y) | -knows_context(x,y) | can_apply(x,y). [clausify(5)].\nunderstands(system,domain). [assumption].\nknows_context(system,domain). [assumption].\n-can_apply(system,domain). [deny(6)].\nend_of_list.\n\nformulas(demodulators).\nend_of_list.\n\n============================== PREDICATE ELIMINATION =================\n\nEliminating understands/2\n7 understands(system,domain). [assumption].\n8 -understands(x,y) | can_explain(x,y). [clausify(1)].\nDerived: can_explain(system,domain). [resolve(7,a,8,a)].\n\nEliminating can_explain/2\n9 can_explain(system,domain). [resolve(7,a,8,a)].\n10 -can_explain(x,y) | knows(x,y). [clausify(2)].\nDerived: knows(system,domain). [resolve(9,a,10,a)].\n\nEliminating knows/2\n11 knows(system,domain). [resolve(9,a,10,a)].\n12 -knows(x,y) | believes(x,y). [clausify(3)].\nDerived: believes(system,domain). [resolve(11,a,12,a)].\n\nEliminating believes/2\n13 believes(system,domain). [resolve(11,a,12,a)].\n14 -believes(x,y) | can_reason_about(x,y). [clausify(4)].\nDerived: can_reason_about(system,domain). [resolve(13,a,14,a)].\n\nEliminating can_reason_about/2\n15 can_reason_about(system,domain). [resolve(13,a,14,a)].\n16 -can_reason_about(x,y) | -knows_context(x,y) | can_apply(x,y). [clausify(5)].\nDerived: -knows_context(system,domain) | can_apply(system,domain). [resolve(15,a,16,a)].\n\nEliminating knows_context/2\n17 -knows_context(system,domain) | can_apply(system,domain). [resolve(15,a,16,a)].\n18 knows_context(system,domain). [assumption].\nDerived: can_apply(system,domain). [resolve(17,a,18,a)].\n\nEliminating can_apply/2\n19 can_apply(system,domain). [resolve(17,a,18,a)].\n20 -can_apply(system,domain). [deny(6)].\nDerived: $F. [resolve(19,a,20,a)].\n\n============================== end predicate elimination =============\n\nAuto_denials: (no changes).\n\nTerm ordering decisions:\nPredicate symbol precedence: predicate_order([ ]).\nFunction symbol precedence: function_order([ ]).\nAfter inverse_order: (no changes).\nUnfolding symbols: (none).\n\nAuto_inference settings:\n % set(neg_binary_resolution). % (HNE depth_diff=0)\n % clear(ordered_res). % (HNE depth_diff=0)\n % set(ur_resolution). % (HNE depth_diff=0)\n % set(ur_resolution) -> set(pos_ur_resolution).\n % set(ur_resolution) -> set(neg_ur_resolution).\n\nAuto_process settings: (no changes).\n\n============================== PROOF =================================\n\n% Proof 1 at 0.00 (+ 0.00) seconds.\n% Length of proof is 21.\n% Level of proof is 8.\n% Maximum clause weight is 0.\n% Given clauses 0.\n\n1 (all x all y (understands(x,y) -> can_explain(x,y))) # label(non_clause). [assumption].\n2 (all x all y (can_explain(x,y) -> knows(x,y))) # label(non_clause). [assumption].\n3 (all x all y (knows(x,y) -> believes(x,y))) # label(non_clause). [assumption].\n4 (all x all y (believes(x,y) -> can_reason_about(x,y))) # label(non_clause). [assumption].\n5 (all x all y (can_reason_about(x,y) & knows_context(x,y) -> can_apply(x,y))) # label(non_clause). [assumption].\n6 can_apply(system,domain) # label(non_clause) # label(goal). [goal].\n7 understands(system,domain). [assumption].\n8 -understands(x,y) | can_explain(x,y). [clausify(1)].\n9 can_explain(system,domain). [resolve(7,a,8,a)].\n10 -can_explain(x,y) | knows(x,y). [clausify(2)].\n11 knows(system,domain). [resolve(9,a,10,a)].\n12 -knows(x,y) | believes(x,y). [clausify(3)].\n13 believes(system,domain). [resolve(11,a,12,a)].\n14 -believes(x,y) | can_reason_about(x,y). [clausify(4)].\n15 can_reason_about(system,domain). [resolve(13,a,14,a)].\n16 -can_reason_about(x,y) | -knows_context(x,y) | can_apply(x,y). [clausify(5)].\n17 -knows_context(system,domain) | can_apply(system,domain). [resolve(15,a,16,a)].\n18 knows_context(system,domain). [assumption].\n19 can_apply(system,domain). [resolve(17,a,18,a)].\n20 -can_apply(system,domain). [deny(6)].\n21 $F. [resolve(19,a,20,a)].\n\n============================== end of proof ==========================\n\n============================== STATISTICS ============================\n\nGiven=0. Generated=1. Kept=0. proofs=1.\nUsable=0. Sos=0. Demods=0. Limbo=0, Disabled=15. Hints=0.\nWeight_deleted=0. Literals_deleted=0.\nForward_subsumed=0. Back_subsumed=0.\nSos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.\nNew_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.\nDemod_attempts=0. Demod_rewrites=0.\nRes_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.\nNonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.\nMegabytes=0.02.\nUser_CPU=0.00, System_CPU=0.00, Wall_clock=0.\n\n============================== end of statistics =====================\n\n============================== end of search =========================\n\nTHEOREM PROVED\n\nExiting with 1 proof.\n\nProcess 27928 exit (max_proofs) Mon Jan 13 16:10:57 2025\n'}

安装

前提条件

• Python 3.12+
• UV 包管理器
• 下载适用于您的平台的 Prover9/Mace4，并进行给定的修复（来自 https://www.cs.unm.edu/~mccune/prover9/gui/v05.html）

设置

1. 将 Prover9/Mace4 安装到已知位置（例如，F:/Prover9-Mace4/）
2. 克隆此存储库
3. 安装依赖项：

uv venv
uv pip install -e .

配置

添加到您的 MCP 环境配置：

{
  "mcpServers": {
    "mcp-logic": {
      "command": "uv",
      "args": [
        "--directory",
        "path/to/mcp-logic/src/mcp_logic",
        "run",
        "mcp_logic",
        "--prover-path",
        "path/to/Prover9-Mace4/bin-win32"
      ]
    }
  }
}

可用工具

prove

使用 Prover9 运行逻辑证明：

{
  "tool": "prove",
  "arguments": {
    "premises": [
      "all x (man(x) -> mortal(x))",
      "man(socrates)"
    ],
    "conclusion": "mortal(socrates)"
  }
}

check-well-formed

验证逻辑语句语法：

{
  "tool": "check-well-formed",
  "arguments": {
    "statements": [
      "all x (man(x) -> mortal(x))",
      "man(socrates)"
    ]
  }
}

文档

请参阅 Documents 文件夹，了解详细的分析和示例：

• 知识到应用：对 AI 系统中理解和实际应用的正式逻辑分析

项目结构

mcp-logic/
├── src/
│   └── mcp_logic/
│       └── server.py    # 主要 MCP 服务器实现
├── tests/
│   ├── test_proofs.py   # 核心功能测试
│   └── test_debug.py    # 调试实用程序
├── Documents/           # 分析和文档
├── pyproject.toml      # Python 包配置
└── README.md          # 此文件

开发

运行测试：

uv pip install pytest
uv run pytest

许可证

MIT