What is Mcp Server Logical Solver

mcp-server-logical-solver is a powerful logical reasoning system that integrates MCP servers with Prover9/Mace4 to facilitate automated reasoning and logical validation. It combines Large Language Models (LLMs) with formal theorem proving capabilities to process logical problems in both natural language and First-Order Logic (FOL) format.

Use cases

Use cases for mcp-server-logical-solver include automating logical problem solving in academic settings, validating logical arguments in research, enhancing AI systems with reasoning capabilities, and providing educational tools for teaching logic and reasoning.

How to use

To use mcp-server-logical-solver, input logical problems in natural language or FOL format following Prover9’s syntax requirements. The system processes these inputs through a two-stage pipeline: first, it conducts a detailed logical analysis using LLM, then it provides a structured summary of the reasoning process. Users can also batch process multiple logical problems.

Key features

Key features of mcp-server-logical-solver include the ability to handle complex logical operations, automated theorem proving through Prover9/Mace4, structured reasoning with LLM-based analysis, and the generation of detailed explanations for logical conclusions.

Where to use

mcp-server-logical-solver can be utilized in various fields such as artificial intelligence, formal verification, education, and any domain requiring logical reasoning and validation of arguments.

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:

# Original FOL with Unicode
∀x (P(x) ∧ Q(x)) → (R(x) ⊕ S(x))

# Translated for Prover9
all x ((P(x) & Q(x)) -> -(R(x) <-> S(x)))

Key Components

1. Logical Solver (main.py)

• Processes logical problems through a two-stage pipeline:
  • First stage: Detailed logical analysis using LLM with Prover9 integration
  • Second stage: Structured summarization of the reasoning process
• Supports batch processing of multiple logical problems
• Provides comprehensive output including premises, conclusions, and explanations

2. Templates (template.py)

• LOGICAL_SOLVER_TEMPLATE: Guides the LLM in logical problem solving
  • Combines natural language and FOL analysis
  • Integrates with Prover9 for formal verification
  • Provides structured reasoning guidelines
• LOGICAL_SUMMARIZER_TEMPLATE: Ensures consistent output format
  • Generates JSON-structured responses
  • Includes explanation, answer, and tool usage information

3. Parser (parser.py)

• Handles FOL formula transformations
• Specializes in XOR operation processing
• Ensures compatibility with Prover9 syntax

4. Prover9 Output Interpretation

The system interprets Prover9’s theorem proving results as follows:

• THEOREM PROVED: Indicates that Prover9 has found a formal proof that the conclusion logically follows from the premises. The system returns “True” in this case.

• SEARCH FAILED: Indicates that Prover9 could not find a proof. This result requires further analysis as it can mean either:

  • “False”: When the premises clearly contradict or do not support the conclusion
  • “Uncertain”: When the premises are insufficient to determine the conclusion’s truth value

The system uses LLM-based analysis to distinguish between “False” and “Uncertain” cases when SEARCH FAILED is encountered.

Prerequisites

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
     

Installation

1. Clone this repository:

   git clone [your-repository-url]
   cd mcp-server-logical-solver
   

2. Install dependencies:

   pip install -r requirements.txt
   

Configuration

1. Environment Variables (.env)

Create a .env file in the root directory with the following settings:

# Model Configuration
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

# Optional Settings
DEBUG=False  # Enable debug mode

2. MCP Configuration (mcp_config.json)

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 .

Running the Project

1. Basic Usage (Single Problem)

python test.py

This will process a sample problem and save the output to output.json.

2. Batch Processing

python main.py input.json output.json

Where:

• input.json: Path to your input file containing logical problems
• output.json: Path where results will be saved

Input JSON format:

Output Format

The system generates structured output in the following format. tool_use indicates whether tool calling was successful:

{
  "premises": "Original natural language premises",
  "premises-FOL": "Processed FOL premises",
  "conclusion": "Natural language conclusion",
  "conclusion-FOL": "FOL conclusion",
  "answer": "True/False/Uncertain",
  "explanation": "Detailed reasoning process",
  "tool_use": "True/False"
}

Troubleshooting

1. MCP Server Connection Issues

   • Verify the MCP-Logic server is running
   • Check the port settings in mcp_config.json
   • Ensure no firewall is blocking the connection

2. Model API Issues

   • Verify your API key in the .env file
   • Check if you have sufficient API credits
   • Ensure the selected model is available for your account

3. Input Format Issues

   • Validate your input JSON format
   • Ensure FOL statements are properly formatted
   • Check for proper Unicode characters in logical symbols