@RyanNg1403
基本信息
A project that integrates mcp servers for Prover9/Mace4 for a logical reasoning agent
使用下面的配置,将此服务器添加到你的 MCP 客户端。
{
"mcpServers": {
"mcp-server-logical-solver": {
"command": "python",
"args": [
"test.py"
]
}
}
}工具列表暂未提供
当前收录暂时没有可展示的工具列表，不代表服务没有工具。请查阅项目文档了解支持的能力。
工具是从 README 中自动提取的。维护者可以在 ## Tools 标题下列出工具,即可填充这部分内容。
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.
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.
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).
Inputs must follow Prover9 syntax: use `all` for ∀, `exists` for ∃, `&` for ∧, `|` for ∨, `->` for →, `<->` for ↔, and `-` for ¬. XOR (⊕) is automatically transformed to an equivalent form.
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).
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.
Yes, by setting the model provider to `ollama` in the `.env` file and running a local model; no API key is required for Ollama.
Hindsight: Agent Memory That Learns
A good sequence diagram can solve almost any communication problem in engineering. Volley lets your agent write them as plain text, with the real request and response payloads on every arrow. It checks its own syntax wi
Yuppsy MCP: build and publish real estate websites from your AI assistant. Yuppsy lets your AI assistant create live websites for real estate agents and individual property listings. You don't need a designer or any code
Request dedicated senior developers to work on your project, write job descriptions, and prep technical interviews — all without leaving your Claude chat. Just describe what you need, and Lemon.io MCP does the rest. 1–3
This open-source curriculum introduces the fundamentals of Model Context Protocol (MCP) through real-world, cross-language examples in .NET, Java, TypeScript, JavaScript, Rust and Python. Designed for developers, it focuses on practical techniques for building modular, scalable,
评论