MCP Server Logical Solver
About
A project that integrates mcp servers for Prover9/Mace4 for a logical reasoning agent
Explore
- Two‑stage pipeline: LLM analysis plus Prover9 verification
- Supports natural language and First‑Order Logic inputs
- Automatic XOR operation transformation for Prover9 compatibility
- Batch processing of multiple logical problems
- JSON‑structured output with explanation and tool usage status
- Multiple model providers: OpenAI, Anthropic, Gemini, Ollama
Setting up with Highlight
This MCP is not yet compatible with Highlight’s one-click setup. However, you can still use it with Highlight by following these steps:
- Download and install Highlight from highlightai.com/download
- Navigate to the plugins tab and select "Add Custom Plugin"
-
Configure the plugin with the settings below
Plugin Name
MCP Server Logical SolverCommand (node, npx, python, etc.)Please refer to the README for specific instructions on how to obtain API keys or other required environment variables.
- Enable "Start Automatically" if you want the plugin to start when Highlight launches
From the repository
Before setting up this project, you need to:
1. Set up the MCP-Logic server:
git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
2. Follow the MCP-Logic setup instructions:
- For Windows:
windows-setup-mcp-logic.bat
- For Linux:
chmod +x linux-setup-script.sh
./linux-setup-script.sh
3. Start the MCP-Logic server:
- For Windows:
run-mcp-logic.bat
- For Linux:
./run-mcp-logic.sh
Create a .env file in the root directory with the following settings:
MODEL_PROVIDER=openai # Options: openai, anthropic, gemini, ollama
MODEL_NAME=gpt-4 # Specify your model name
API_KEY=your_api_key_here # Required for OpenAI/Anthropic/Gemini
Change the file mcp_config_example.json to mcp_config.json in the root directory:
{
"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"
]
}
}
}
Make sure to adjust the --prover-path and --directory values to match where you cloned MCP-Logic .
python test.py
``
This will process a sample problem and save the output to Claude Desktop / Cursor
Paste into your MCP client config file to install this server.
{
"mcpServers": {
"mcp server logical solver": {
"mcp-server-logical-solver": {
"command": "python",
"args": [
"test.py"
]
}
}
}
}McpServers
{
"mcp-server-logical-solver": {
"command": "python",
"args": [
"test.py"
]
}
}A powerful logical reasoning system that combines Large Language Models (LLMs) with formal theorem proving capabilities. This project leverages the MCP-Logic server to provide automated reasoning and logical validation.
Overview
This system is designed to:
- Process logical problems in both natural language and First-Order Logic (FOL) format
- Utilize automated theorem proving through Prover9/Mace4
- Provide structured reasoning with LLM-based analysis
- Handle complex logical operations including XOR transformations
- Generate detailed explanations for logical conclusions
FOL Input Requirements
The First-Order Logic (FOL) inputs must strictly follow Prover9's syntax requirements:
1. Logical Operators:
- Universal Quantifier: ∀ (translated to 'all')
- Existential Quantifier: ∃ (translated to 'exists')
- Conjunction: ∧ (translated to '&')
- Disjunction: ∨ (translated to '|')
- Implication: → (translated to '->')
- Bi-implication: ↔ (translated to '<->')
- Negation: ¬ (translated to '-')
- XOR operations: ⊕ (automatically transformed to equivalent forms)
2. Format Guidelines:
- Premises and conclusions must be well-formed formulas
- Variables and predicates should follow Prover9's naming conventions
- XOR expressions are automatically converted to their equivalent forms using negation and bi-implication
Example:
```prover9
Sign in to leave a review
Use Google, GitHub, or an email account so ratings stay tied to real people.
No reviews posted yet.
