MCP Logic

🚀 MCP-Logic 服務器

MCP-Logic服務器是一個提供自動化推理能力的MCP服務器，藉助Prover9/Mace4為AI系統賦予邏輯推理功能。它通過簡潔的MCP接口，實現定理證明和邏輯模型驗證，有效解決了AI系統在邏輯推理方面的需求。

🚀 快速開始

MCP-Logic服務器專為AI系統設計，通過簡潔的MCP接口實現定理證明和邏輯模型驗證。以下是一個簡單的使用示例，展示如何使用該服務器進行邏輯推理：

# 證明理解加上上下文能夠應用於實際
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系統打造，支持自動化推理。
• 知識驗證：能夠對知識表示及其邏輯推論進行正式驗證。
• 無縫集成：與模型上下文協議（MCP）生態系統完美兼容。
• 深度推理：支持複雜邏輯證明，包括嵌套量詞和多前提推理。
• 實際應用：特別適用於AI知識模型和推理鏈的驗證。
• 與Prover9無縫集成：支持定理自動證明。
• 支持複雜邏輯：支持複雜的邏輯公式和證明。
• 語法驗證：內置語法驗證功能。
• 乾淨接口：搭配有MCP協議的乾淨服務器接口。
• 完善處理：具備完善的錯誤處理和日誌記錄。
• 推理分析：支持知識表示及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二進制文件

💻 使用示例

基礎用法

# 證明理解加上上下文能夠應用於實際
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. 因此，通過邏輯推理得出蘇格拉底是有生命的結論。

📚 詳細文檔

可用工具

1. 定理證明工具

{
  "tool": "prove-theorem",
  "arguments": {
    "premises": [
      "所有人類都是有生命的生物。",
      "蘇格拉底是人。"
    ],
    "conclusion": "蘇格拉底是有生命的。"
  }
}

2. 語法驗證工具

{
  "tool": "check-well-formed",
  "arguments": {
    "statements": [
      "所有人類都是有生命的生物。",
      "蘇格拉底是人。"
    ]
  }
}

項目結構

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許可證。