Schema | FOL Prover MCP Server

FOL Prover MCP Server

Describes the environment variables required to run the server.

Name	Required	Description	Default
No arguments

Features and capabilities supported by this server

Capability	Details
`tools`	{ "listChanged": false }
`experimental`	{}

Functions exposed to the LLM to take actions

Name	Description
proveA	Execute a FOL proof. Attempts to prove the conclusion from the given premises using the specified theorem prover (vampire, eprover, or prover9).
prove_sessionB	Execute a proof using the current session's premises and conclusion.
add_premiseA	Add a premise (axiom) to the current session for incremental proof building.
set_conclusionC	Set the conclusion (goal) to prove in the current session.
clear_sessionA	Clear all premises and conclusion from a session.
get_sessionA	Get the current state of a session including all premises and conclusion.
parse_formulaA	Parse and validate a FOL formula. Returns information about variables, constants, predicates, and whether the formula is syntactically valid.
convert_to_tptpC	Convert a FOL problem to TPTP format (standard format for theorem provers).
list_proversA	List available theorem provers and their status.
create_sessionB	Create a new named session for proof building.
list_sessionsA	List all active sessions.
switch_sessionB	Switch to a different session.
remove_premiseB	Remove a premise by index from the current session.

Interactive templates invoked by user choice

Name	Description
No prompts

Contextual data attached and managed by the client

Name	Description
No resources

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/NewJerseyStyle/folprover-mcp'

If you have feedback or need assistance with the MCP directory API, please join our Discord server