MCP Logic

🚀 MCP-Logic Server

An MCP server that provides automated reasoning capabilities, using Prover9/Mace4 to offer logical reasoning functions for AI systems. This server enables theorem proving and logical model verification through a concise MCP interface.

🚀 Quick Start

The MCP-Logic Server bridges the gap between AI and formal logic through an interface specifically designed for AI systems. It offers automated reasoning capabilities and seamless integration with the MCP ecosystem, making it ideal for validating AI knowledge models and inference chains.

✨ Features

• AI-Centric Design: Tailored for AI systems, supporting automated reasoning.
• Knowledge Validation: Enables formal verification of knowledge representations and their logical inferences.
• Seamless Integration: Fully compatible with the Model Context Protocol (MCP) ecosystem.
• Deep Reasoning: Supports complex logical proofs, including nested quantifiers and multi-premise reasoning.
• Practical Application: Particularly suitable for validating AI knowledge models and inference chains.

💻 Usage Examples

Basic Usage

# Prove that understanding plus context can be applied in practice
if __name__ == "__main__":
    knowledge = [
        "All humans are mortal beings.",          # Premise 1: man(x) → mortal(x)
        "Socrates is a human."                    # Premise 2: man(socrates)
    ]
    conclusion = "Socrates is mortal."
    run_knowledge_to_application(knowledge, conclusion)

Output

All humans are mortal beings.  # Premise 1: man(x) → mortal(x)
Socrates is a human.             # Premise 2: man(socrates)
Conclusion: Socrates is mortal.   # Conclusion: mortal(socrates)
Proof:
1. According to Premise 1, the definition of humans dictates that all humans are mortal.
2. Premise 2 states that Socrates falls within the category of humans.
3. Therefore, through logical reasoning, we conclude that Socrates is mortal.

📦 Installation

System Requirements

• Operating System: Linux/macOS/Windows
• Memory: At least 4GB RAM recommended
• Disk Space: At least 10GB of available space

Installation Steps

# Download the project source code
git clone https://github.com/yourusername/mcp-logic.git
cd mcp-logic

# Run the setup script (choose the appropriate script based on your system)
# For Linux/macOS:
./setup-script.sh

# For Windows:
./setup-script.bat

# After installation, a ladr directory containing Prover9 binaries will be generated

📚 Documentation

Tool Invocation Examples

1. Theorem Proving Tool

{
  "tool": "prove-theorem",
  "arguments": {
    "premises": [
      "All humans are mortal beings.",
      "Socrates is a human."
    ],
    "conclusion": "Socrates is mortal."
  }
}

2. Syntax Validation Tool

{
  "tool": "check-well-formed",
  "arguments": {
    "statements": [
      "All humans are mortal beings.",
      "Socrates is a human."
    ]
  }
}

Project Structure

mcp-logic/
├── src/
│   └── mcp_logic/
│       └── server.py           # Main MCP server implementation file
├── tests/
│   ├── test_proofs.py          # Core functionality test cases
│   └── test_debug.py           # Debugging tool tests
├── Documents/                  # Analysis and documentation
├── pyproject.toml              # Python package configuration file
├── setup-script.sh             # Setup script (install LADR and 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 (without Docker)
└── README.md                   # Project description document

Note: After running the setup script, a ladr folder containing Prover9 binaries will be generated in the project directory, but this folder will not be included in the repository version control.

Development Guide

Running Test Cases

uv pip install pytest
uv run pytest

📄 License

This project is licensed under the MIT License.