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: 10Example
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")
# => {:ok, :theorem}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
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.
Queries all available provers on SystemOnTPTP and returns results from systems
that did not error out. Returns a list of tuples {system_id, result}.
Makes a single request to SystemOnTPTP to run all given systems with default
arguments. Accepted options are the same as for query_system/3.
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.
Functions
@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 (default5);:raw— return the raw prover output instead of interpreting it (defaultfalse);:url— override the SystemOnTPTP endpoint URL.
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.