Index of values

Call the prover (if present) on the given problem, and return a result.

Call the prover, and also tries to parse a TSTP derivation, if the prover succeeded

Same as CallProver.call, but also returns the raw output of the prover

Use E to convert a set of statements into CNF

Max depth of the proof

explore the surrounding of this list of declarations, returning the TPTP output of E

find_file name dir looks for a file with the given name, recursively, in dir, or in its parent dir recursively.

Force the lazy proof step, if any

Obtain the ID of the proof step.

Find the name of the declaration, or

Check whether some include declaration can be found in the sequence

Is the proof a proper DAG?

List of registered provers

Lookup a prover by its name.

Name of the prover

Try to extract a proof from a list of TSTP statements.

Parse file using the input format chosen by the user

Try to parse a proof from a file.

parse_file ~recursive file parses file

Parsing a TPTP file is here presented with a recursive option that, if true, will make "include" directives to be recursively parsed.

parse lexbuf.

Given a lexbuf, try to parse its content into a sequence of untyped declarations

parse stdin.

Print proof step, and its parents

print the whole proofs

Register the prover with the given name.

Run Eproof_ram, and tries to read a proof back.

Runs E with the given input (optional verbosity level).

Number of nodes in the proof

Traversal of parent proofs

Traverse the proof.