AtpClient

DOI

Elixir client for external automated theorem provers. Four backends are supported:

The TPTP language itself — reading, linting, printing, the SZS ontology — is the tptp library's; this one is the transport to the provers.

Every backend takes an AtpClient.Problem — a binary, a Tptp.File or a Tptp.Unit — and returns {:ok, %AtpClient.Result{}} or {:error, reason}. A result's status is the system's SZS verdict as a value of Tptp.Szs.Ontology (:theorem, :unsatisfiable, :counter_satisfiable, :satisfiable, :gave_up, :timeout, …), read from the system's output by AtpClient.Verdict; the output itself, the delimited proof blocks and how the status was obtained travel with it. Semantically distinct verdicts stay distinct (:theorem ≠ :unsatisfiable, :counter_satisfiable ≠ :satisfiable), and a status word the ontology does not define is reported rather than turned into an atom. {:error, reason} means no status could be obtained: a network failure, a missing binary, output with no status line.

A backend never parses what it sends. A binary goes to the prover as it is, a Tptp.File as the source it was read from, a Tptp.Unit as its statements sliced from their files — so the direct path from TPTP text to prover costs nothing beyond the transport. AtpClient.preflight/1 is the explicit check for callers who want one before a round-trip.

Each backend also implements the AtpClient.Backend behaviour (config_key/0, label/0, config_schema/0, verify/1, query/2), so a Smart Cell or other UI can enumerate backends via AtpClient.backends/0, render their settings from config_schema/0, probe reachability with verify/1, and run a TPTP problem with the uniform query/2 entry point — without hard-coding per-backend knowledge.

Installation

Add :atp_client to your dependencies in mix.exs:

def deps do
  [
    {:atp_client, "~> 0.7"}
  ]
end

Configuration

Settings are resolved from three sources, in increasing precedence:

  1. Library defaults (declared in AtpClient's mix.exs).
  2. Application environment (typically config/config.exs).
  3. Per-call keyword options passed to the relevant function.

Only the settings required by the backends you actually use need to be set.

# config/config.exs
import Config

config :atp_client, :sotptp,
  # The default points at tptp.org; override for a mirror or internal
  # deployment:
  url: "https://tptp.org/cgi-bin/SystemOnTPTPFormReply",
  default_time_limit_sec: 10

config :atp_client, :starexec,
  base_url: "https://starexec.example.org/starexec",
  username: System.get_env("STAREXEC_USER"),
  password: System.get_env("STAREXEC_PASS")

config :atp_client, :isabelle,
  host: "isabelle.example.org",
  port: 9999,
  password: System.get_env("ISABELLE_PASSWORD"),
  # Directory shared between this node and the Isabelle server. If the two
  # see the same files under different paths (e.g. because one runs inside
  # a container), set `isabelle_dir` separately:
  local_dir: "/shared/problems",
  isabelle_dir: "/shared/problems",
  session: "HOL"

config :atp_client, :local_exec,
  binary: "eprover",
  args: ["--auto", "--tstp-format", "--cpu-limit=10"],
  cpu_timeout_s: 10

Any setting may be overridden for a single call:

AtpClient.LocalExec.query(problem, binary: "vampire", args: ["--mode", "casc"])

Usage

SystemOnTPTP

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

AtpClient.SystemOnTptp.list_provers()
# => ["Alt-Ergo---0.95.2", "Beagle---0.9.52", ...]

# A bare name runs the version SystemOnTPTP currently advertises; an
# identifier from list_provers/0 names one exactly.
{:ok, result} = AtpClient.SystemOnTptp.query_system(problem, "cvc5", time_limit_sec: 10)
result.status    # => :theorem
result.system    # => "cvc5---1.3.4"
result.evidence  # => :szs
result.output    # => the prover's stdout as SystemOnTPTP relayed it

{:ok, outcomes} =
  AtpClient.SystemOnTptp.query_selected_systems(problem, ["cvc5", "Vampire", "Nope"], time_limit_sec: 5)

for {system, outcome} <- outcomes do
  case outcome do
    {:ok, result} -> {system, result.status}
    {:error, reason} -> {system, reason}
  end
end
# => [{"cvc5---1.3.4", :theorem}, {"Vampire---5.0.1", :theorem}, {"Nope", {:unknown_system, "Nope"}}]

AtpClient.SystemOnTptp.query_all_systems(problem, time_limit_sec: 5)
# => {:ok, [{"Alt-Ergo---0.95.2", {:ok, %AtpClient.Result{status: :theorem}}}, ...]}

A problem read with tptp is sent as the text it was read from, and a problem whose include directives were resolved locally is sent expanded:

{:ok, file, []} = Tptp.from_file("Problems/PUZ/PUZ001+1.p")
AtpClient.SystemOnTptp.query_system(file, "E")

{:ok, unit, []} = Tptp.Unit.from_file("my_problem.p", resolver: Tptp.Resolver.Fs)
AtpClient.LocalExec.query(unit, binary: "eprover")

StarExec

{:ok, session} = AtpClient.StarExec.login()

{:ok, response} =
  AtpClient.StarExec.create_job(session, %{
    "name" => "smoke-test",
    "sid" => 42,
    "queue" => 1,
    "cpuTimeout" => 30,
    "wallclockTimeout" => 30,
    # ... solver / benchmark fields as your instance expects
  })

job_id = extract_job_id(response)   # deployment-specific

{:ok, info} = AtpClient.StarExec.wait_for_job(session, job_id, timeout_ms: 600_000)

# Pair stdout is read the same way as SystemOnTPTP output:
{:ok, zip} = AtpClient.StarExec.get_job_output(session, job_id)
{:ok, result} = AtpClient.Verdict.interpret(stdout_from(zip), AtpClient.StarExec)
result.status
# => :theorem

AtpClient.StarExec.logout(session)

StarExec's job-creation form accepts a large, version-dependent set of fields; create_job/3 therefore takes an open-ended map and leaves the exact field names to the caller. The request/4 low-level helper is available for any endpoint this module does not wrap directly.

Isabelle

Isabelle needs a running isabelle server to talk to. If isabelle is on your PATH (or reachable via ISABELLE_TOOL), the bundled isabelle_elixir package can start one for you — no manual isabelle server invocation required:

{:ok, server} = IsabelleClient.start_server()
opts = [host: server.host, port: server.port, password: server.password]

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

# Bare-body input is auto-wrapped in `theory ... imports Main begin ... end`.
{:ok, session} = AtpClient.Isabelle.open_session(opts)
{:ok, %{status: :theorem}} = AtpClient.Isabelle.prove_theory(session, theory, "Example")
:ok = AtpClient.Isabelle.close_session(session)

# When you're done:
IsabelleClient.Server.kill(server.name)

Point at an already-running server by dropping the start_server/0 call and supplying the coordinates directly, either per-call or via config.exs. In containerised or Cygwin setups where the BEAM and Isabelle see the shared theory directory under different paths, set both :local_dir (BEAM view) and :isabelle_dir (server view); when they match, only :local_dir (or neither — it defaults to a subdirectory of System.tmp_dir!/0) is needed.

Sessions are cheap to keep open and expensive to restart. Reuse one across multiple theories:

{:ok, session} = AtpClient.Isabelle.open_session(opts)
try do
  {:ok, %{status: :theorem}} = AtpClient.Isabelle.prove_theory(session, theory, "Example")
  {:ok, %{status: :theorem}} = AtpClient.Isabelle.prove_theory(session, other_theory, "Other")
after
  AtpClient.Isabelle.close_session(session)
end

Pass a TPTP/THF problem to query/2 (or prove_tptp/3 with a session) to route it through IsabelleClient.TPTP.isabellize_theory/1; the result's status is the weakest link over the conjectures and details.lemmas has each one's own:

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

{:ok, result} = AtpClient.Isabelle.query(problem, opts)
result.status          # => :theorem
result.details.lemmas  # => [%{name: "g", status: :theorem}]

Isabelle prints no SZS lines; its status is read from the server's messages (result.evidence is {:backend, AtpClient.Isabelle}), and the full use_theories payload is in result.details.payload.

LocalExec

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

# `binary` is resolved against $PATH or used as an absolute path; `args`
# may contain "{{problem}}" to pin the problem-file position (otherwise the
# path is appended last).
{:ok, result} =
  AtpClient.LocalExec.query(problem,
    binary: "eprover",
    args: ["--auto", "--tstp-format", "--cpu-limit=10"]
  )

result.status
# => :theorem

# A proof the prover delimited with `SZS output start … end` is read as TPTP,
# with each formula's inference record intact:
{:ok, proof, []} = AtpClient.Result.proof(result)
Enum.map(proof.statements, & &1.name.text)

# A file already on disk is handed to the prover by path; nothing is read or
# copied, and the prover resolves its includes itself.
AtpClient.LocalExec.query_file("Problems/PUZ/PUZ001+1.p", binary: "eprover")

scripts/build_eprover.sh builds the E theorem prover from source and installs it into priv/bin/ for use as the LocalExec binary.

Uniform backend interface

Every backend module also implements AtpClient.Backend, which is what the Smart Cell uses to render a configuration form and dispatch a run:

for module <- AtpClient.backends() do
  %{
    key:    module.config_key(),    # :sotptp | :starexec | :isabelle | :local_exec
    label:  module.label(),         # "SystemOnTPTP", "StarExec", ...
    fields: module.config_schema()  # [%AtpClient.Config.Field{...}, ...]
  }
end

# Once a form is filled out, probe reachability before submitting work:
AtpClient.StarExec.verify(
  base_url: "https://starexec.example.org",
  username: "...",
  password: "..."
)
# => :ok | {:error, reason}

# And run a problem through any backend uniformly:
AtpClient.LocalExec.query(problem, binary: "eprover")
AtpClient.SystemOnTptp.query(problem)                          # runs E
AtpClient.SystemOnTptp.query(problem, default_system: "cvc5")

# `AtpClient.query/3` adds the one thing a backend never does on its own —
# reading and linting the problem first:
AtpClient.query(AtpClient.LocalExec, problem, binary: "eprover", preflight: true)
# => {:error, {:invalid_problem, [%Tptp.Diagnostic{}, ...]}} for a problem that does not parse

Analyzers

AtpClient.Analyzer.Tptp4x runs the TPTP World's own checker, TPTP4X, on the SystemOnTPTP deployment as a Tptp.Analyzer, so an editor can add its findings to Tptp.Lint's:

analysis = Tptp.analyze(source)

Tptp.Analyzer.run_all(analysis, [Tptp.Lint, AtpClient.Analyzer.Tptp4x])
# => [{:tptp_lint, [...]}, {:tptp4x, [...]}]

License

MIT.