AtpClient (AtpClient v0.7.2)

Copy Markdown View Source

Elixir client for external automated theorem provers.

Four backends are supported:

Each backend implements AtpClient.Backend: query/2 takes an AtpClient.Problem and returns {:ok, %AtpClient.Result{}} or {:error, reason}.

Problems and results

A problem is a binary, a Tptp.File or a Tptp.Unit; see AtpClient.Problem for what each sends. A backend never parses what it sends. preflight/1 is the explicit check for callers who want one — an editor, say — before a round-trip to a prover.

A result's status is a value of Tptp.Szs.Ontology, read from the system's output by AtpClient.Verdict; see AtpClient.Result for the rest of what it carries.

{:ok, result} = AtpClient.LocalExec.query("fof(c, conjecture, $true).", binary: "eprover")
result.status      # :theorem
result.evidence    # :szs
result.output      # E's stdout

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"),
  session: "HOL"

# Same-host setups need nothing more — `:local_dir` defaults to a
# subdirectory of `System.tmp_dir!/0`. Only set `:local_dir` and
# `:isabelle_dir` when the two sides see the directory under different
# paths (containers, Cygwin).

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"])

Summary

Functions

backends()

Returns the modules implementing AtpClient.Backend. Iterate this in a configuration UI to discover what's wireable without hard-coding the list.

preflight(problem)

Reads and lints the problem with Tptp.analyze/2, without sending it anywhere.

query(backend, problem, opts \\ [])

Runs problem on backend, optionally checking it first.

Functions

backends()

@spec backends() :: [module()]

Returns the modules implementing AtpClient.Backend. Iterate this in a configuration UI to discover what's wireable without hard-coding the list.

preflight(problem)

@spec preflight(AtpClient.Problem.t()) ::
  :ok | {:error, {:invalid_problem, [Tptp.Diagnostic.t()]}}

Reads and lints the problem with Tptp.analyze/2, without sending it anywhere.

A Tptp.File or Tptp.Unit is analysed as it is; anything else is parsed from its bytes first. Returns :ok when no diagnostic is an error, and {:error, {:invalid_problem, diagnostics}} with every diagnostic, warnings included, otherwise. The analysis costs what Tptp.analyze/2 costs — a traversal, and for a binary a parse — which is why no backend does it on its own.

iex> AtpClient.preflight("fof(a, axiom, p).")
:ok

iex> {:error, {:invalid_problem, diagnostics}} = AtpClient.preflight("fof(a, axiom, p")
iex> Tptp.Diagnostic.any_errors?(diagnostics)
true

query(backend, problem, opts \\ [])

@spec query(module(), AtpClient.Problem.t(), keyword()) ::
  {:ok, AtpClient.Result.t()} | {:error, term()}

Runs problem on backend, optionally checking it first.

Equivalent to backend.query(problem, opts) with one option of its own:

  • :preflight — when true, preflight/1 runs first and an invalid problem is {:error, {:invalid_problem, diagnostics}} without any round-trip. Defaults to false: the direct path parses nothing.

    AtpClient.query(AtpClient.SystemOnTptp, problem, preflight: true, time_limit_sec: 10)