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

执照

麻省理工学院

This server cannot be installed

security - not tested

license - permissive license

quality - not tested

hybrid server

The server is able to function both locally and remotely, depending on the configuration or use case.

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

Related Resources

Reddit Discussion about this server

Related MCP Servers

Deepseek Thinker MCP Server
ruixingshi
A
security
F
license
A
quality
Provides reasoning content to MCP-enabled AI clients by interfacing with Deepseek's API or a local Ollama server, enabling focused reasoning and thought process visualization.
Last updated -
1
54
24
JavaScript
think-mcp-server
marcopesani
-
security
A
license
-
quality
A minimal MCP Server that provides Claude AI models with the 'think' tool capability, enabling better performance on complex reasoning tasks by allowing the model to pause during response generation for additional thinking steps.
Last updated -
525
1
TypeScript
MIT License
Unleash Feature Flag MCP Server
ylin6
-
security
F
license
-
quality
An MCP server that allows AI assistants to programmatically manage Unleash feature flags through natural language, enabling operations like creating, updating, and retrieving feature flags across projects.
Last updated -
5
2
TypeScript
Think MCP Tool
Rai220
-
security
-
license
-
quality
An MCP server that provides a "think" tool enabling structured reasoning for AI agents, allowing them to pause and record explicit thoughts during complex tasks or multi-step tool use.
Last updated -
1
Python
MIT License

View all related MCP servers

MCP-Logic

MCP逻辑

设计理念

特征

快速示例

安装

先决条件

设置

使用 Docker-不知道这是否正常工作，主要设计用于直接与 Claude Desktop 一起使用

Claude 桌面集成

可用工具

证明

检查格式是否正确

文档

项目结构

发展

执照

Related Resources

Related MCP Servers

Deepseek Thinker MCP Server

think-mcp-server

Unleash Feature Flag MCP Server

Think MCP Tool

Appeared in Searches

New MCP Servers

MCP directory API