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:

[
  {
    "premises": "Natural language premises...",
    "premises-FOL": "First order logic premises...",
    "conclusion": "Natural language conclusion...",
    "conclusion-FOL": "First order logic conclusion...",
    "label": "True/False/Uncertain"  // Optional ground truth
  }
]

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