FOL Prover MCP Server

Example Use Cases

• 1

  Perform first-order logic theorem proving with support for multiple provers.

• 2

  Build and manage incremental proof sessions with named contexts.

• 3

  Parse, validate, and convert FOL formulas to TPTP format.

Description

This MCP server enables incremental first-order logic theorem proving with support for multiple external provers and a built-in resolution-based prover requiring no external installation. It supports Unicode and ASCII FOL notation, session management for building proofs incrementally, and conversion to the standard TPTP format. The server automatically falls back to alternative provers if one fails, providing robust proof attempts. It is suitable for integration with clients like Claude Desktop and VS Code with Continue.