MCP Server Logical Solver
About
A project that integrates mcp servers for Prover9/Mace4 for a logical reasoning agent
Details
- Author
- RyanNg1403
- GitHub stars
- 1
- Downloads
- 239
- Categories
- Other
Jump to
- 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
Clone the repository, install dependencies with pip install -r requirements.txt, configure a .env file with your model provider and API key, and set up mcp_config.json to point to the MCP‑Logic server. Run a single problem with python test.py or batch process via python main.py input.json output.json.
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"
]
}
}MCP Server Logical Solver
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.
