@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.
A one-of-a-kind resume builder that keeps your privacy in mind. Completely secure, customizable, portable, open-source and free forever. Try it out today!
Painless E2E Automation for Mobile and Web
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
DeepMark helps teachers deliver rapid, consistent marking with meaningful feedback for every student — in a fraction of the time. What once took a week, now takes one free period.
Model Context Protocol Servers
コメント