AtpClient.SystemOnTptp (AtpClient v0.7.0)

Public tptp.org HTTP form API; see query_system/3 and query_all_systems/2.

Configuration

config :atp_client, :sotptp,
  url: "tptp.example.org/SystemOnTPTPFormReply",
  auto_refresh: true,
  refresh_timeout_ms: 100_000,
  default_time_limit_sec: 10

Example

thf_problem = """
thf(conj,conjecture,
  ![X: $o]: (X | ~X)
).
"""

# system IDs returned by list_provers/0, e.g. "Vampire-FMo---5.0.1"
{:ok, result} = AtpClient.SystemOnTptp.query_system(thf_problem, "Vampire-FMo---5.0.1")
result.status   # => :theorem
result.output   # => the prover's stdout as SystemOnTPTP relayed it

Cancellation

SystemOnTPTP exposes no remote cancellation endpoint — the form submits a problem and the server runs the prover to its TimeLimit, returning the prover stdout in the HTTP response. When the calling BEAM process dies the in-flight Req/Finch request errors out and the connection slot is released, but the remote prover continues to its TimeLimit. The only server-side bound on cancelled work is the :time_limit_sec option passed to query_system/3.

Summary

Functions

list_provers()

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.

query_all_systems(problem, opts \\ [])

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

query_selected_systems(problem, system_ids, opts \\ [])

Makes a single request to SystemOnTPTP to run all given systems with default arguments. Accepted options are the same as for query_system/3; the :command, :format, and :transform overrides — if set — are applied identically to every system in system_ids.

query_system(problem, system_id, opts \\ [])

Queries a specific system via SystemOnTPTP. Available systems can be looked up with list_provers/0. The problem is an AtpClient.Problem in a dialect the selected system accepts; SystemOnTPTP resolves include directives against its own copy of the TPTP library, so a Tptp.File is sent as it is.

Functions

list_provers()

@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.

query_all_systems(problem, opts \\ [])

@spec query_all_systems(AtpClient.Problem.t(), Keyword.t()) ::
  {:ok,
   [
     {String.t(),
      {:ok, AtpClient.Result.t()} | {:error, AtpClient.Verdict.failure()}}
   ]}
  | {: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.

query_selected_systems(problem, system_ids, opts \\ [])

@spec query_selected_systems(AtpClient.Problem.t(), [String.t()], Keyword.t()) ::
  {:ok,
   [
     {String.t(),
      {:ok, AtpClient.Result.t()} | {:error, AtpClient.Verdict.failure()}}
   ]}
  | {:error, term()}

Returns one {system_id, outcome} per section of the reply, where outcome is what AtpClient.Verdict.interpret/3 read from that system's output.

query_system(problem, system_id, opts \\ [])

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

The response body — the system's stdout as SystemOnTPTP relays it — is read by AtpClient.Verdict and kept on the result as output.

Options

:time_limit_sec — time limit in seconds (default 5);
:url — override the SystemOnTPTP endpoint URL;
:command, :format, :transform — per-system SotP form overrides (Command___<sysid>, Format___<sysid>, Transform___<sysid>). Each is transmitted only when set. :format and :transform are honoured by tptp.org — passing an unknown module name causes SotP to reply with ERROR: Formatter did not create .... :command is transmitted for compatibility with self-hosted SotP deployments but the tptp.org public endpoint currently ignores it and runs its own wrapper.

Cancellation

SystemOnTPTP has no remote-cancel endpoint. If the calling process dies the Finch connection is released locally, but the prover runs to its TimeLimit on the server. Set :time_limit_sec to bound the server- side work; that is the only knob available.