FOL Prover

소개

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.

주요 기능

• Supports multiple external theorem provers (Vampire, E, Prover9)
• Includes a built-in simple, resolution-based prover
• Parses and validates first-order logic formulas with Unicode notation
• 1 GitHub stars
• Manages proofs incrementally using named sessions
• Converts logical problems to standard TPTP format

사용 사례

• Executing complex first-order logic proofs directly or incrementally
• Validating first-order logic formulas and converting them to TPTP format
• Integrating logical reasoning capabilities into AI development environments or educational tools