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)
).
"""
# A system name resolves to the version SystemOnTPTP currently
# advertises; an identifier from list_provers/0 names one exactly.
{:ok, result} = AtpClient.SystemOnTptp.query_system(thf_problem, "Vampire")
result.status # => :theorem
result.system # => "Vampire---5.0.1"
result.output # => the prover's stdout as SystemOnTPTP relayed itSystems
SystemOnTPTP identifies a system as <name>---<version> and keeps only the
current version of each, so a version string in a caller's code goes stale
with the next deployment. Every function here takes a bare name as well and
resolves it to the latest version advertised, through
AtpClient.SystemOnTptp.Provers.resolve/2; an identifier is checked as
written. A system that is neither is {:error, {:unknown_system, name}} and
is not submitted — SystemOnTPTP stops processing a request at the first
system it does not know, so an unknown one would silently take every system
after it down with it.
query/2 runs :default_system, "E" unless configured otherwise.
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; the
:command, :format, and :transform overrides — if set — are applied
identically to every system in systems.
Queries one system via SystemOnTPTP, given by name ("E") or identifier
("E---3.5.1"); see "Systems" in the module documentation. 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
@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(AtpClient.Problem.t(), Keyword.t()) :: {:ok, [{String.t(), {:ok, AtpClient.Result.t()} | {:error, term()}}]} | {: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(AtpClient.Problem.t(), [String.t()], Keyword.t()) :: {:ok, [{String.t(), {:ok, AtpClient.Result.t()} | {:error, term()}}]} | {: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; the
:command, :format, and :transform overrides — if set — are applied
identically to every system in systems.
Returns one {system, outcome} per system given, in the order given, where
system is the resolved identifier and outcome is what
AtpClient.Verdict.interpret/3 read from that system's output. A system
that is not advertised is {name, {:error, {:unknown_system, name}}} and is
not submitted; one the deployment accepted but returned no section for is
{id, {:error, :no_output}}. Only the outer {:error, reason} is a failed
request.
@spec query_system(AtpClient.Problem.t(), String.t(), Keyword.t()) :: {:ok, AtpClient.Result.t()} | {:error, term()}
Queries one system via SystemOnTPTP, given by name ("E") or identifier
("E---3.5.1"); see "Systems" in the module documentation. 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.
Returns {:error, {:unknown_system, system}} without a round-trip when the
system is not advertised.
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 (default5);: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.:formatand:transformare honoured by tptp.org — passing an unknown module name causes SotP to reply withERROR: Formatter did not create ....:commandis 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.