Acerca de
The FOL Prover is an MCP (Model Context Protocol) server dedicated to first-order logic (FOL) theorem proving. It serves as an accessible interface for interacting with powerful, established theorem provers such as Vampire, E, and Prover9, while also offering a standalone, built-in resolution-based prover that requires no external dependencies. This tool is designed to integrate seamlessly with MCP clients like Claude Desktop and VS Code with Continue, empowering users to parse and validate FOL formulas, manage proofs incrementally through named sessions, and convert problems to the standard TPTP format. Its automatic fallback mechanism enhances reliability by attempting multiple provers, making advanced logical reasoning more robust and integrated into development workflows.
