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
image
image
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
Run the setup script:
Windows run:
Linux/macOS:
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
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:
Replace "/path/to/mcp-logic" with your actual repository path.
Available Tools
image
prove
Run logical proofs using Prover9:
check-well-formed
Validate logical statement syntax:
Documentation
See the Documents folder for detailed analysis and examples:
- Knowledge to Application: A formal logical analysis of understanding and practical application in AI systems
Project Structure
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:
License
MIT
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
image
image
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
Run the setup script:
Windows run:
Linux/macOS:
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
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:
Replace "/path/to/mcp-logic" with your actual repository path.
Available Tools
image
prove
Run logical proofs using Prover9:
check-well-formed
Validate logical statement syntax:
Documentation
See the Documents folder for detailed analysis and examples:
- Knowledge to Application: A formal logical analysis of understanding and practical application in AI systems
Project Structure
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:
License
MIT