We’re a group of researchers working on neurosymbolic AI, and we wanted to share a tool we’ve built: PrologMCP, an MCP server that exposes SWI-Prolog to LLM agents.
We’re aware of the other Prolog MCP servers announced on this forum, including Jan’s MCP pack. Ours has a different purpose: it’s aimed at agents that offload reasoning to Prolog and then need to inspect and revise their own formalizations.
The part we found really challenging was exposing proof trees to the agent. The interactive debugger is not accessible programmatically, so we ended up writing a custom meta-interpreter that returns a structured call tree with per-node success/failure status.
If this is useful or interesting to you, we’d be glad to hear any feedback.
Nice! Do you have an assessment on how well this works?
The mcp Prolog pack version I wrote exposes the Prolog toplevel to the LLM. This means it can notably
Start/stop/control multiple Prolog instances
Load files
Pose queries
Run the interactive debugger
Run the coverage analysis tool
Run the profiler.
This notably targets program development though, not so much logic/knowledge representation. I still have to tell Claude to actually use this. It typically just puts print statements in the code and runs it non-interactively when trying to debug a Prolog program.
Thank you! We evaluated it, and the results are reported in this paper:
However, the meta-interpreter was not necessary in this case. Overall:
The LLMs used the MCP server seamlessly, but the only tools invoked were create_session (consult_text at the time) and run_goal.
The models (Claude Sonnet 4.6, GPT-4.1, and o4-mini) produced syntactically correct Prolog code on the first attempt. The few failures to derive the correct answer stemmed from GPT-4.1 failing to adhere to unconventional dataset semantics; nevertheless, the generated code was syntactically correct.
Overall, it worked very well, but the task only required the LLMs to produce short snippets of very simple code.
Thank you for the resources. Evaluating the self-debugging of generated formalizations is one of our next steps.