@spec list_provers() :: [String.t()]

Returns a list with all available system identifiers from SystemOnTPTP that correspond to known provers. This excludes type checking systems etc. which also get returned by the API.

@spec query_all_systems(String.t(), Keyword.t()) ::
  {:ok, [{String.t(), AtpClient.ResultNormalization.atp_result()}]}
  | {:ok, [{String.t(), String.t()}]}
  | {:error, term()}

Queries all available provers on SystemOnTPTP and returns results from systems that did not error out. Returns a list of tuples {system_id, result}.

All options accepted by query_selected_systems/3 are forwarded.

@spec query_selected_systems(String.t(), [String.t()], Keyword.t()) ::
  {:ok, [{String.t(), AtpClient.ResultNormalization.atp_result()}]}
  | {:ok, [{String.t(), String.t()}]}
  | {:error, term()}

Makes a single request to SystemOnTPTP to run all given systems with default arguments. Accepted options are the same as for query_system/3.

@spec query_system(String.t(), String.t(), Keyword.t()) ::
  {:ok, String.t()}
  | AtpClient.ResultNormalization.atp_result()
  | {:error, term()}

Queries a specific system via SystemOnTPTP. Available systems can be looked up with list_provers/0. The problem is expected to be in valid TPTP format and compatible with the selected prover.

Options

• :time_limit_sec — time limit in seconds (default 5);
• :raw — return the raw prover output instead of interpreting it (default false);
• :url — override the SystemOnTPTP endpoint URL.