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

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

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

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

Clear all premises and conclusion from a session.

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

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

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

List available theorem provers and their status.

Create a new named session for proof building.

List all active sessions.

Switch to a different session.

Remove a premise by index from the current session.