# 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](https://github.com/angrysky56/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
# 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:
   ```bash
   git clone https://github.com/angrysky56/mcp-logic
   cd mcp-logic
   ```

2. Follow the MCP-Logic setup instructions:
   - For Windows:
     ```bash
     windows-setup-mcp-logic.bat
     ```
   - For Linux:
     ```bash
     chmod +x linux-setup-script.sh
     ./linux-setup-script.sh
     ```

3. Start the MCP-Logic server:
   - For Windows:
     ```bash
     run-mcp-logic.bat
     ```
   - For Linux:
     ```bash
     ./run-mcp-logic.sh
     ```

## Installation

1. Clone this repository:
   ```bash
   git clone [your-repository-url]
   cd mcp-server-logical-solver
   ```

2. Install dependencies:
   ```bash
   pip install -r requirements.txt
   ```

## Configuration

### 1. Environment Variables (.env)
Create a `.env` file in the root directory with the following settings:
```env
# 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:
```json
{
  "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](https://github.com/angrysky56/mcp-logic) .

## Running the Project

### 1. Basic Usage (Single Problem)
```bash
python test.py
```
This will process a sample problem and save the output to `output.json`.

### 2. Batch Processing
```bash
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:
```json
[
  {
    "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:
```json
{
    "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