MCP-Logic
An MCP server providing automated reasoning capabilities using Prover9/Mace4 for AI systems. This server enables logical theorem proving and logical model verification through a clean MCP interface.
Design Philosophy
MCP-Logic bridges the gap between AI systems and formal logic by providing a robust interface to Prover9/Mace4. What makes it special:
- AI-First Design: Built specifically for AI systems to perform automated reasoning
- Knowledge Validation: Enables formal verification of knowledge representations and logical implications
- Clean Integration: Seamless integration with the Model Context Protocol (MCP) ecosystem
- Deep Reasoning: Support for complex logical proofs with nested quantifiers and multiple premises
- Real-World Applications: Particularly useful for validating AI knowledge models and reasoning chains
Features
- Seamless integration with Prover9 for automated theorem proving
- Support for complex logical formulas and proofs
- Built-in syntax validation
- Clean MCP server interface
- Extensive error handling and logging
- Support for knowledge representation and reasoning about AI systems
Quick Example
# 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!
Installation
Prerequisites
- Python 3.10+
- UV package manager
- Git for cloning the repository
- CMake and build tools (for building LADR/Prover9)
Setup
Clone this repository
git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
Run the setup script:
Windows run:
windows-setup-mcp-logic.bat
Linux/macOS:
chmod +x linux-setup-script.sh
./linux-setup-script.sh
The setup script:
- Checks for dependencies (git, cmake, build tools)
- Downloads LADR (Prover9/Mace4) from the external repository: laitep/LADR
- Builds the LADR library to create Prover9 binaries in the ladr/bin directory
- Creates a Python virtual environment
- Sets up configuration files for running with or without Docker
IMPORTANT: The LADR directory is not included in the repository itself and will be installed through the setup script or manually.
Using Docker- no idea if this is working right, mainly designed for direct use with Claude Desktop
If you prefer to run with Docker this script:
- Finds an available port
- Activates the virtual environment
- Runs the server with the correct paths to the installed Prover9
# Linux/macOS
./run-mcp-logic.sh
# Windows
run-mcp-logic.bat
These scripts will build and run a Docker container with the necessary environment.
Claude Desktop Integration
To use MCP-Logic with Claude Desktop, use this configuration:
{
"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"
]
}
}
}
Replace "/path/to/mcp-logic" with your actual repository path.
prove
Run logical proofs using Prover9:
{
"tool": "prove",
"arguments": {
"premises": [
"all x (man(x) -> mortal(x))",
"man(socrates)"
],
"conclusion": "mortal(socrates)"
}
}
Validate logical statement syntax:
{
"tool": "check-well-formed",
"arguments": {
"statements": [
"all x (man(x) -> mortal(x))",
"man(socrates)"
]
}
}
Documentation
See the Documents folder for detailed analysis and examples:
Project Structure
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
Note: After running setup-script.sh, a "ladr" directory will be created containing the Prover9 binaries, but this directory is not included in the repository itself.
Development
Run tests:
uv pip install pytest
uv run pytest
License
MIT