AtpClient — end-to-end demo

Setup

Mix.install([
  {:atp_client, "~> 0.8"}
])

atp_client exposes a single, normalized interface to four backends for automated theorem provers. This notebook walks through each backend with a runnable problem — no external servers to configure by hand for the same-host paths.

Every backend takes an AtpClient.Input — a binary, a Tptp.File or a Tptp.Unit — and returns {:ok, %AtpClient.Result{}} (the system asserted a verdict) or {:error, reason} (none could be obtained). The result's status is the SZS Ontology value as a Tptp.Szs.Ontology atom (:theorem, :unsatisfiable, :satisfiable, :counter_satisfiable, :gave_up, :timeout, …); its output is the system's output verbatim, and evidence says how the status was read.

alias AtpClient.{SystemOnTptp, Isabelle, LocalExec, StarExec}

SystemOnTPTP

The public tptp.org HTTP form. No configuration needed — the default URL already points at https://tptp.org/cgi-bin/SystemOnTPTPFormReply.

problem = ~S"""
fof(ax1, axiom, p).
fof(ax2, axiom, (p => q)).
fof(goal, conjecture, q).
"""

systems/1 lists the systems the deployment offers, filtered by what they can do. The list starts from the snapshot shipped with the library and is refreshed from the deployment in the background.

SystemOnTptp.systems(capability: :prove) |> Enum.map(& &1.id) |> Enum.take(10)

Run a single system, by name: "Zipperpin" resolves to the version SystemOnTPTP currently advertises, which the result's system names. The prover's stdout travels with the result as output.

with {:ok, result} <- SystemOnTptp.query_system(problem, "Zipperpin", time_limit_sec: 5),
do: {result.system, result.status}

with {:ok, result} <- SystemOnTptp.query_system(problem, "Zipperpin", time_limit_sec: 5),
do: IO.puts(result.output)

Fan out to several systems in one HTTP round-trip. Every system given comes back, in the order given: a result, or the reason there is none — a first-order-only solver handed a higher-order problem, a name the deployment does not advertise.

with {:ok, outcomes} <-
  SystemOnTptp.query_selected_systems(
    problem,
    ["cvc5", "Z3", "Nope"],
    time_limit_sec: 15
  ),
do: outcomes

query_all_systems/2 runs every system with the :prove capability and is convenient for benchmarking, but it holds one HTTP connection open for the sum of the per-system time limits — set :time_limit_sec conservatively.

Isabelle/HOL

AtpClient.Isabelle talks to an isabelle server. When isabelle is on $PATH (or reachable via the ISABELLE_TOOL env var), the bundled :isabelle_elixir package can spin one up for you — no manual server management.

{:ok, server} =
  IsabelleClient.start_server(
    server_name: "atp_client_demo_#{System.unique_integer([:positive])}"
  )

opts = [
  host: server.host,
  port: server.port,
  password: server.password
]

:local_dir defaults to a subdirectory of System.tmp_dir!/0, so the same-host case (Isabelle running next to the BEAM) is zero-config. In containers or Cygwin where the two see the same directory under different paths, set :local_dir (BEAM view) and :isabelle_dir (server view) explicitly.

Pass either a full theory or just a body — bare text is auto-wrapped in theory <name> imports Main begin ... end. prove_theory/4 returns the same %AtpClient.Result{} every other backend does; Isabelle prints no SZS lines, so the status is read from the server's messages and the result's evidence is {:backend, AtpClient.Isabelle}.

body = ~S"""
lemma "\<forall>x. P x \<longrightarrow> P x"
  by auto
"""

{:ok, session} = Isabelle.open_session(opts)
try do
  Isabelle.prove_theory(session, body, "Reflexivity")
after
  Isabelle.close_session(session)
end

For TPTP/THF problems, query/2 routes through IsabelleClient.TPTP.isabellize_theory/1, injects the configured :proof_method (default "by auto"), and reads one status per conjecture into result.details.lemmas. Names come from the input formulae.

tptp_problem = ~S"""
thf(p_type, type, p: $i > $o).
thf(g_taut, conjecture, ! [X: $i]: (p @ X | ~ (p @ X))).
thf(g_false, conjecture, ! [X: $i]: (p @ X & ~ (p @ X))).
"""

with {:ok, result} <-
       Isabelle.query(
         tptp_problem,
         opts ++ [proof_method: "sledgehammer nitpick oops", use_theories_timeout_ms: 600_000]
       ),
     do: result.details.lemmas

g_taut should come back :theorem (sledgehammer found a proof), g_false as :counter_satisfiable (nitpick found a counter-model). The verdict comes from the tool's own message, so oops — which withdraws the goal so Isabelle keeps checking the next lemma — is fine.

The session is what's expensive to start (~seconds for HOL); each prove_theory/4 call over an open one is fast. The block above already demonstrates the pattern.

Shut the server down when you're done with it:

IsabelleClient.Server.kill(server.name)

LocalExec

Runs a locally installed TPTP-compliant prover binary (E, Vampire, …) via a port. The BEAM watches both a prover-side --cpu-limit (encoded in :args) and a wall-clock kill timer, and both arrive as a :timeout status — the kill appends its own SZS line to whatever the prover printed.

Point :binary at whatever is on PATH (or an absolute path). Each prover spells the CPU limit differently, so it goes in :args:

LocalExec.query(problem,
  binary: "eprover",
  args: ["--auto", "--tstp-format", "--cpu-limit=10"],
  cpu_timeout_s: 10
)

If the binary is missing you get {:error, {:prover_not_found, name}} rather than a crash — cheap to probe reachability before committing to a run:

LocalExec.verify(binary: "definitely-not-a-prover")

scripts/build_eprover.sh in the source tree builds E from source into priv/bin/eprover if you want a self-contained install.

StarExec

Self-hosted StarExec (Tomcat) instances, driven through the same URLs the web UI uses. Nothing to demo without credentials, so this section only shows the shape:

{:ok, session} =
  StarExec.login(
    base_url: "https://starexec.example.org",
    username: System.get_env("STAREXEC_USER"),
    password: System.get_env("STAREXEC_PASS")
  )

# End-to-end: upload problem, run against the configured solver, wait,
# fetch stdout, classify.
StarExec.prove(session, problem,
  space_id: 42,
  solver_cfg_id: 137,
  cpu_timeout_s: 30
)

StarExec.logout(session)

Death of the process running prove/3 cancels the remote job (via delete_job/3), so Task.shutdown/2 is the natural way to enforce a wall-clock budget on top.

Uniform interface

Every backend module implements AtpClient.Backend, so a UI can enumerate backends, render each one's config_schema/0 as a form, probe reachability with verify/1, and dispatch a problem with query/2 — without hard-coding per-backend knowledge.

for module <- AtpClient.backends() do
  %{
    key: module.config_key(),
    label: module.label(),
    fields: length(module.config_schema())
  }
end