MCP Server Logical Solver

Name: MCP Server Logical Solver
Author: RyanNg1403

@RyanNg1403

代码仓库

关于 MCP Server Logical Solver

A project that integrates mcp servers for Prover9/Mace4 for a logical reasoning agent

#mcp-server #logical-solver #theorem-proving

基本信息

分类

其他

运行时

python

传输方式

stdio

发布者

RyanNg1403

配置

使用下面的配置,将此服务器添加到你的 MCP 客户端。

{
  "mcpServers": {
    "mcp-server-logical-solver": {
      "command": "python",
      "args": [
        "test.py"
      ]
    }
  }
}

工具

未检测到工具

工具是从 README 中自动提取的。维护者可以在 ## Tools 标题下列出工具,即可填充这部分内容。

概览

What is MCP Server Logical Solver?

MCP Server Logical Solver is a logical reasoning system that combines Large Language Models (LLMs) with formal theorem proving through Prover9/Mace4. It processes logical problems in natural language and First‑Order Logic (FOL) to provide automated reasoning and structured explanations.

How to use MCP Server Logical Solver?

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.

Key features of MCP Server Logical Solver

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

Use cases of MCP Server Logical Solver

Validating logical conclusions from natural language premises
Formal theorem proving with Prover9 and Mace4
Automated reasoning for research or educational tasks
Generating detailed, step‑by‑step logical explanations

FAQ from MCP Server Logical Solver

How does MCP Server Logical Solver handle “SEARCH FAILED” from Prover9?

When Prover9 cannot find a proof, the system uses LLM‑based analysis to distinguish between a “False” result (premises contradict the conclusion) and an “Uncertain” result (insufficient premises).

What FOL syntax is required for inputs?

Inputs must follow Prover9 syntax: use all for ∀, exists for ∃, & for ∧, | for ∨, -> for →, <-> for ↔, and - for ¬. XOR (⊕) is automatically transformed to an equivalent form.

What dependencies are needed to run MCP Server Logical Solver?

You must have the MCP‑Logic server installed and running, Python 3, the packages in requirements.txt, and an API key for the chosen LLM provider (unless using Ollama).

How does the output look?

The system returns a JSON object containing original premises/conclusions (natural language and FOL), the answer (True/False/Uncertain), a detailed explanation, and a tool_use boolean indicating whether tool calling succeeded.