Skip to main content
Glama
NewJerseyStyle

FOL Prover MCP Server

FOL Prover MCP Server

An MCP (Model Context Protocol) server for First-Order Logic theorem proving using Vampire, E, and Prover9.

Features

  • Multiple Provers: Support for Vampire, E (eprover), Prover9, and built-in simple prover

  • Built-in Prover: Simple resolution-based prover requires no external installation

  • FOL Parsing: Parse and validate first-order logic formulas with Unicode notation

  • Session Management: Build proofs incrementally with named sessions

  • TPTP Export: Convert problems to standard TPTP format

  • Automatic Fallback: Try multiple provers if one fails

Related MCP server: Pyke MCP Server

Installation

Prerequisites

The server includes a built-in simple prover that works without any external installation. For more complex proofs, install one of the following theorem provers:

Vampire (recommended):

# Linux (Ubuntu/Debian)
sudo apt-get install vampire

# macOS (with Homebrew)
brew install vampire

# Or download from: https://github.com/vprover/vampire

E Prover:

# Linux (Ubuntu/Debian)
sudo apt-get install eprover

# macOS
brew install eprover

# Or download from: https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html

Prover9:

# Download from: https://www.cs.unm.edu/~mccune/prover9/

Install the MCP Server

pip install folprover-mcp

Or install from source:

git clone https://github.com/folprover-mcp/folprover-mcp
cd folprover-mcp
pip install -e .

Configuration

Add to your MCP client configuration:

Claude Desktop

Add to ~/.config/claude/claude_desktop_config.json (Linux/macOS) or %APPDATA%\Claude\claude_desktop_config.json (Windows):

{
  "mcpServers": {
    "folprover": {
      "command": "folprover-mcp"
    }
  }
}

VS Code with Continue

Add to your Continue configuration:

{
  "mcpServers": {
    "folprover": {
      "command": "folprover-mcp"
    }
  }
}

Usage

FOL Notation

The server supports standard FOL notation with Unicode operators:

Symbol

Meaning

Example

Universal quantifier

∀x P(x)

Existential quantifier

∃x P(x)

Conjunction (AND)

P(x) ∧ Q(x)

Disjunction (OR)

P(x) ∨ Q(x)

Implication

P(x) → Q(x)

Biconditional

P(x) ↔ Q(x)

¬

Negation

¬P(x)

Exclusive OR

P(x) ⊕ Q(x)

You can also use ASCII alternatives:

  • forall or all for

  • exists for

  • & or and for

  • | or or for

  • -> or implies for

  • <-> or iff for

  • ~ or not for ¬

Tools

prove

Execute a FOL proof directly:

{
  "premises": [
    "∀x (Human(x) → Mortal(x))",
    "Human(socrates)"
  ],
  "conclusion": "Mortal(socrates)",
  "prover": "vampire"
}

add_premise

Add a premise to the current session:

{
  "premise": "∀x (Human(x) → Mortal(x))"
}

set_conclusion

Set the conclusion to prove:

{
  "conclusion": "Mortal(socrates)"
}

prove_session

Prove using the current session's premises and conclusion:

{
  "prover": "vampire"
}

parse_formula

Parse and validate a FOL formula:

{
  "formula": "∀x (P(x) → Q(x))"
}

convert_to_tptp

Convert a problem to TPTP format:

{
  "premises": ["∀x (P(x) → Q(x))", "P(a)"],
  "conclusion": "Q(a)"
}

list_provers

List available theorem provers:

{}

Session Management

  • create_session: Create a new named session

  • list_sessions: List all active sessions

  • switch_session: Switch to a different session

  • get_session: Get current session state

  • clear_session: Clear all premises and conclusion

  • remove_premise: Remove a premise by index

Examples

Example 1: Classic Syllogism

Premises:

  1. All humans are mortal: ∀x (Human(x) → Mortal(x))

  2. Socrates is human: Human(socrates)

Conclusion: Socrates is mortal: Mortal(socrates)

Result: Theorem (True)

Example 2: Set Theory

Premises:

  1. If x is a subset of y and y is a subset of z, then x is a subset of z: ∀x ∀y ∀z ((Subset(x,y) ∧ Subset(y,z)) → Subset(x,z))

  2. A is a subset of B: Subset(a, b)

  3. B is a subset of C: Subset(b, c)

Conclusion: A is a subset of C: Subset(a, c)

Result: Theorem (True)

Example 3: With Counter-model

Premises:

  1. Some birds can fly: ∃x (Bird(x) ∧ CanFly(x))

Conclusion: All birds can fly: ∀x (Bird(x) → CanFly(x))

Result: Not a theorem (False - there's a counter-model where some bird can't fly)

Architecture

folprover-mcp/
├── src/folprover_mcp/
│   ├── __init__.py
│   ├── server.py          # MCP server implementation
│   ├── provers.py         # Prover interfaces (Vampire, E, Prover9, Simple)
│   ├── simple_prover.py   # Built-in resolution prover
│   ├── fol_parser.py      # FOL formula parser
│   └── tptp_converter.py  # TPTP format converter
├── tests/                 # Test suite
├── examples/              # Example proof problems
├── pyproject.toml
└── README.md

References

License

MIT License

Available Tools

13 tools
add_premiseA

Add a premise (axiom) to the current session for incremental proof building.

ParametersJSON Schema
NameRequiredDescriptionDefault
premiseYesFOL formula to add as a premise
sessionNoSession name (defaults to current session)

TDQS

A3.6/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations, the description carries the full burden for behavioral disclosure. It states 'Add' (mutation) but does not discuss side effects, duplicate handling, validation, or session constraints. Minimal transparency.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

A single sentence that is front-loaded with the action and resource. No unnecessary words, though it could be slightly more structured with a break for parameter details.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness3/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool's simplicity (2 params, no output schema), the description is adequate but lacks information on return value or behavior for existing premises. It covers the basic purpose but leaves some questions unanswered.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100%, so the schema already documents both parameters. The description adds no extra meaning beyond naming the concept ('premise') and context ('session'). Baseline score of 3 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description uses a specific verb 'add' and resource 'premise', and includes context ('current session for incremental proof building'). It clearly distinguishes from siblings like remove_premise and prove.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description implies usage for adding axioms during incremental proof building. It does not explicitly state when not to use or mention alternatives, but the context and sibling list make the intended usage clear.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

clear_sessionA

Clear all premises and conclusion from a session.

ParametersJSON Schema
NameRequiredDescriptionDefault
sessionNoSession name to clear (defaults to current session)

TDQS

A3.8/5.0
Behavior3/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations provided, the description carries the full burden of disclosure. It correctly indicates a destructive action ('clear') but does not mention whether the action is reversible, if it affects other sessions, or any side effects. Acceptable but not thorough.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

A single sentence that conveys the exact behavior without any unnecessary words. Highly concise and front-loaded.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool's simplicity (one optional parameter, no output schema), the description sufficiently covers the core functionality. It could mention return behavior, but this is not critical for a clear action. Completeness is high for the complexity level.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, so the baseline is 3. The description does not add meaning beyond the schema, which already describes the ''session'' parameter. No additional semantic value is provided.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the action ('Clear') and the resource ('all premises and conclusion from a session'). It distinguishes from siblings like 'remove_premise' and 'set_conclusion' by indicating a bulk reset rather than individual modification.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description implies usage for resetting a session but provides no explicit guidance on when to use versus alternatives. No exclusions or context for when not to use are given, though the purpose is straightforward.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

convert_to_tptpC

Convert a FOL problem to TPTP format (standard format for theorem provers).

ParametersJSON Schema
NameRequiredDescriptionDefault
premisesYesList of premise formulas
conclusionYesConclusion formula

TDQS

C2.9/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations, the description carries full behavioral transparency burden. It does not disclose side effects, output format, error conditions, or any constraints. The description is too brief to inform the agent about behavioral traits.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is concise, with one focused sentence. It is front-loaded with the core action. However, it could be slightly expanded to include output format without losing conciseness.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Without an output schema, the description should explain what the conversion produces (e.g., a string, file path). It only vaguely mentions 'TPTP format' and does not clarify if the output is a string representation. Missing details on valid input formats and error handling.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The input schema has 100% description coverage, already documenting premises and conclusion clearly. The description adds no additional meaning beyond the schema, so a baseline of 3 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool converts a FOL problem to TPTP format, with a brief explanation of TPTP as standard for theorem provers. It gives a clear verb-resource pairing, but lacks explicit linkage to the input parameters (premises and conclusion) and does not fully distinguish from siblings like parse_formula.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No guidance on when to use this tool versus alternatives (e.g., parse_formula, prove) is provided. The description only states what it does, not the appropriate context or prerequisites.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

create_sessionB

Create a new named session for proof building.

ParametersJSON Schema
NameRequiredDescriptionDefault
nameYesName for the new session

TDQS

B3/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations are provided, and the description only states 'Create a new named session' without disclosing behavioral traits such as side effects, authorization needs, or what happens on duplicate names.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness3/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is a single sentence of 8 words, which is efficient, but it lacks necessary details about the tool's behavior and usage, making it too brief to be fully useful.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the complexity of the proof building context and the number of sibling tools, the description does not explain what a session is, what the created session can be used for, or any return information. It is incomplete for an agent to understand the full context.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100% for the sole parameter 'name'. The description adds the word 'named', but this is already implied by the parameter definition. No additional semantic value is provided beyond the schema.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the verb 'create', the resource 'session', and specifies it is for 'proof building'. It distinguishes from sibling tools like 'list_sessions' and 'switch_session'.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No guidance on when to use this tool versus alternatives like 'switch_session'. The description does not mention prerequisites or scenarios.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

get_sessionA

Get the current state of a session including all premises and conclusion.

ParametersJSON Schema
NameRequiredDescriptionDefault
sessionNoSession name (defaults to current session)

TDQS

A3.8/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations provided, so description carries full burden. It states 'get' implying read-only, and specifies what is included (premises and conclusion). Missing details like whether it modifies state or requires permissions, but clear it's a read operation.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Single sentence effectively conveys purpose. No redundancy; front-loaded with key information.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Despite only 1 optional param and no output schema, description adequately explains what is returned. Could mention error conditions or format, but for a simple retrieval tool it is sufficient given sibling tools provide context.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Input schema has 1 parameter with description of type and default. Schema coverage is 100%. Description adds no further parameter semantics beyond noting the return includes premises and conclusion, which is about output not input.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

Description clearly states the tool retrieves the current state of a session including premises and conclusion. Verb 'get' and resource 'current state' are specific, distinguishing it from siblings like 'list_sessions' which lists all sessions.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No guidance on when to use this tool versus alternatives like 'switch_session' or 'create_session'. The description does not mention, implicit or explicit, when this is appropriate.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

list_proversA

List available theorem provers and their status.

ParametersJSON Schema
NameRequiredDescriptionDefault

No parameters

TDQS

A3.7/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations exist, so the description bears full burden. It discloses that the tool lists provers and their status, but does not mention read-only behavior, side effects, or any required permissions. Minimal behavioral context beyond the action itself.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Single sentence, front-loaded with the verb, no wasted words. Highly concise.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness3/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

While the tool is simple with no parameters and no output schema, the description could hint at the return format (e.g., list of names and statuses). It is minimally adequate but lacks completeness for an agent to know what to expect.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

No parameters in the schema, so the description does not need to elaborate. Schema coverage is 100% (trivially). Baseline 4 for zero-parameter tools.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description uses a specific verb 'list' with a clear resource 'theorem provers' and scope 'and their status'. It uniquely identifies the tool among siblings, none of which list provers.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No explicit when or when-not guidance is provided. The description is straightforward, but given the simplicity of the tool (no parameters), it implies use when you need to see available provers. No alternatives mentioned.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

list_sessionsA

List all active sessions.

ParametersJSON Schema
NameRequiredDescriptionDefault

No parameters

TDQS

A3.6/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations are present, so the description carries full burden. It only states the basic action without disclosing behavioral traits such as whether it is read-only, what happens with no sessions, or authentication requirements.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is very short and front-loaded, with no wasted words.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Despite no output schema or parameters, the description is too minimal. It does not explain the return format, sorting, or any additional context, leaving the agent underinformed.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The input schema has no parameters, so the description does not need to add parameter meaning. Baseline score of 4 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool lists all active sessions, distinguishing it from sibling tools like get_session which targets a specific session, and create_session which creates a session.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No explicit when-to-use or when-not-to-use guidance is provided. The context implies it is for listing all active sessions, but alternatives like get_session are not mentioned.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

parse_formulaA

Parse and validate a FOL formula. Returns information about variables, constants, predicates, and whether the formula is syntactically valid.

ParametersJSON Schema
NameRequiredDescriptionDefault
formulaYesFOL formula to parse

TDQS

A4/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations are provided, so the description carries the full burden. It discloses that the tool returns parsed information and validation status, which is transparent. However, it does not explicitly state that the operation is read-only and non-destructive.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is two sentences, front-loads the main purpose, and contains no redundant words. Every sentence adds value.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given only one parameter and no output schema, the description is fairly complete. It explains the tool's operation and return information. A minor gap is the lack of mention of error handling for invalid formulas.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

There is only one parameter ('formula') and the schema already describes it as 'FOL formula to parse'. The description adds no additional meaning beyond what the schema provides. Since schema description coverage is 100%, the baseline score of 3 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

Description clearly states the tool parses and validates FOL formulas, listing specific return information (variables, constants, predicates, syntactic validity). This distinguishes it from sibling tools which focus on session management or proving.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Description implies usage for validating or extracting components from FOL formulas but does not provide explicit guidance on when to use this tool versus alternatives, nor when not to use it.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

proveA

Execute a FOL proof. Attempts to prove the conclusion from the given premises using the specified theorem prover (vampire, eprover, or prover9).

ParametersJSON Schema
NameRequiredDescriptionDefault
premisesYesList of premise formulas in FOL notation. Supports Unicode operators: ∀ (forall), ∃ (exists), ∧ (and), ∨ (or), → (implies), ↔ (iff), ¬ (not)
conclusionYesThe conclusion to prove from the premises
proverNoWhich theorem prover to use (simple is built-in, others require installation)vampire
timeoutNoTimeout in seconds for the proof attempt

TDQS

A3.6/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations, the description carries full burden. It discloses basic behavior (attempts proof, uses specified prover, installation requirements) but omits critical details like return value (proof object or success/failure), timeout behavior, and side effects on sessions.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is a single, front-loaded sentence with no wasted words, efficiently conveying the core purpose and key detail about prover types.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

No output schema is provided, yet the description does not explain what the tool returns (proof, success/failure, errors). It also does not clarify if the tool operates within a session context, leaving a significant gap given the tool's complexity.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, so baseline is 3. The description adds value for the 'prover' parameter by noting 'simple' is built-in and others require installation, which goes beyond the schema enum descriptions.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the verb ('prove'), resource ('FOL proof'), and specifies the provers available, distinguishing it from sibling tools like 'prove_session' and 'parse_formula'.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description implies usage for proving a conclusion from premises but does not explicitly state when to use this tool versus alternatives like 'prove_session' or when not to use it. It mentions installation requirements for some provers, offering minimal guidance.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

prove_sessionB

Execute a proof using the current session's premises and conclusion.

ParametersJSON Schema
NameRequiredDescriptionDefault
proverNoWhich theorem prover to use (simple is built-in, others require installation)vampire
sessionNoSession name (defaults to current session)

TDQS

B3.1/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations exist, and the description only states 'Execute a proof'—no disclosure of side effects, performance, or what happens internally (e.g., output location). This is insufficient for behavioral transparency.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is a single succinct sentence. It is appropriately sized, though slightly terse.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given no annotations, no output schema, and sibling tools like 'prove', the description lacks information on return values, error cases, or how to interpret results. It feels incomplete for a non-trivial tool.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, so the schema already describes both parameters. The description adds no extra meaning beyond what's in the schema, thus baseline score of 3.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the verb 'Execute a proof' and the resource 'current session's premises and conclusion.' It distinguishes from sibling 'prove' by implying session context, but does not explicitly contrast them.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Implies that a session with premises and conclusion must be set up beforehand, but provides no explicit when-to-use or alternatives like 'prove' for ad-hoc proofs.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

remove_premiseB

Remove a premise by index from the current session.

ParametersJSON Schema
NameRequiredDescriptionDefault
indexYesIndex of the premise to remove (0-based)
sessionNoSession name (defaults to current session)

TDQS

B3.1/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations are provided, so the description carries full burden. It describes the mutation (removing a premise) but does not disclose behavior on invalid indexes, side effects on session state, or whether the action is reversible. This lack of detail reduces transparency.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is a single sentence, front-loaded with the action and key parameter. It is efficient and free of unnecessary words, though slightly terse for a complete tool description.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool's simplicity (2 params, no complex nesting or output schema), the description is minimally adequate. It omits error handling, return values (if any), and session existence assumptions. A more complete description would improve agent reliability.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%: both parameters have descriptions in the schema. The description adds 'by index' which reinforces the index parameter, but otherwise adds no new meaning beyond the schema. Baseline score of 3 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the action ('Remove a premise') and the method ('by index') and context ('from the current session'). It distinguishes well from sibling tools like add_premise and clear_session.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No guidance on when to use this tool versus alternatives. For example, it doesn't mention that clear_session would remove all premises, or that index must be valid. Sibling names imply context but the description itself provides no usage advice.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

set_conclusionC

Set the conclusion (goal) to prove in the current session.

ParametersJSON Schema
NameRequiredDescriptionDefault
conclusionYesFOL formula to prove
sessionNoSession name (defaults to current session)

TDQS

C2.8/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations, the description carries the full burden of disclosing behaviors. It does not indicate if setting a conclusion overwrites a previous one, what happens with invalid formulas, or that it is a prerequisite for 'prove'. The description is too terse to be informative about behavior.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness3/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is very concise with 9 words, but it lacks key information about usage and behavior. While front-loaded, it is arguably too brief for a tool with two parameters and no surrounding context.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given no output schema or annotations, the description should provide more context, such as the relationship to sibling tools (e.g., that 'prove' uses this conclusion) and error conditions. It is not complete for a tool that is part of a proving workflow.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The input schema already has 100% coverage with descriptions for both parameters ('FOL formula to prove' and 'Session name'). The description adds no additional parameter details beyond the schema, thus meeting the baseline for high coverage.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool's purpose: setting the conclusion (goal) for a session. It uses a specific verb 'set' and identifies the resource 'conclusion'. While it differentiates from sibling tools like 'prove' or 'add_premise' by focusing on the goal setting, it could be more explicit about the scope.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No guidance is provided on when to use this tool versus alternatives such as 'add_premise' or 'prove'. The description does not mention prerequisites (e.g., a session must exist) or typical usage patterns.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

switch_sessionB

Switch to a different session.

ParametersJSON Schema
NameRequiredDescriptionDefault
nameYesSession name to switch to

TDQS

B3.2/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations, the description must fully disclose behavior. It fails to mention what happens to the active session, whether the switch is immediate, or if there are side effects (e.g., losing unsaved state). The one-line description is insufficient for behavioral transparency.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is a single, focused sentence with no fluff. It is front-loaded with the action and resource, meeting the conciseness criterion perfectly.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool's role in a theorem-proving system with many sibling tools, the description lacks context about the impact of switching sessions (e.g., how it affects ongoing proofs, whether the session is pre-existing). Without an output schema, more detail on return value or side effects is needed.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100% (one parameter with a clear description: 'Session name to switch to'). The tool description adds no additional meaning beyond what the schema already provides, so a baseline of 3 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the action ('Switch') and the resource ('a different session'), effectively distinguishing it from sibling tools like `create_session`, `get_session`, or `list_sessions`. The verb+resource combination is specific and unambiguous.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No guidance is provided on when to use this tool versus alternatives such as `create_session`, `get_session`, or `clear_session`. The description lacks context about prerequisites, scenarios, or when not to use it.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Tool Schema Changelog

Recent tool additions, removals, and schema changes observed during successful MCP inspections. Dates show when Glama detected each change.

  1. 13 tool updatesv0.1.0
    • First observedadd_premise
    • First observedclear_session
    • First observedconvert_to_tptp
    • First observedcreate_session
    • First observedget_session
    • First observedlist_provers
    • First observedlist_sessions
    • First observedparse_formula
    • First observedprove
    • First observedprove_session
    • First observedremove_premise
    • First observedset_conclusion
    • First observedswitch_session

TDQS

A3.7/5.0
Disambiguation5/5

Each tool has a clear, distinct purpose. There is no overlap between adding/removing premises, setting conclusions, managing sessions, parsing formulas, or executing proofs. The two prove tools are differentiated by whether they use session state or direct inputs.

Naming Consistency5/5

All tool names follow a consistent verb_noun pattern in snake_case, such as add_premise, clear_session, list_provers, and set_conclusion. The verbs are descriptive and uniform.

Tool Count5/5

With 13 tools, the surface is well-scoped for a FOL prover server. It covers session management, formula parsing, multiple theorem provers, and TPTP conversion without excess.

Completeness4/5

The tool set covers the full proof workflow: create session, add premises, set conclusion, parse formulas, run proofs, and manage sessions. Minor gaps exist, such as no direct 'update premise' tool, but removing and re-adding works around this.

Maintenance

ActivityInactive
ResponsivenessNo issues

Resources

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Related MCP Connectors

Related MCP Servers

  • A
    license
    Not graded
    quality
    B
    maintenance
    MCP-Logic is a server that provides AI systems with automated reasoning capabilities, enabling logical theorem proving and model verification using Prover9/Mace4 through a clean MCP interface.
    46
    MIT
  • A
    license
    Not graded
    quality
    C
    maintenance
    An MCP server for the Pyke logic programming engine that enables LLMs to perform logical reasoning using knowledge bases with facts, rules, and queries. It supports session management, forward chaining inference, and bulk loading of programs in Logic-LLM format.
    MIT
  • F
    license
    Not graded
    quality
    D
    maintenance
    An MCP server that provides formal reasoning and argument validation tools for AI agents based on established computational argumentation theories. It enables structured argument analysis, defeasible reasoning, and dialogue management using frameworks like Dung, Toulmin, and Walton's schemes.
    -

Latest Blog Posts

MCP directory API

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