AtpClient (AtpClient v0.1.3)

Elixir client for external automated theorem provers.

Three backends are supported:

• SystemOnTPTP — public tptp.org HTTP form API; see AtpClient.SystemOnTptp.
• StarExec — self-hosted StarExec instances; see AtpClient.StarExec.
• Isabelle — isabelle server instances via isabelle_elixir; see AtpClient.Isabelle.

Each backend reads its settings through AtpClient.Config, which layers config/config.exs on top of the library defaults and lets per-call options override everything. See the AtpClient.Config module docs for details.

This package was developed at the University of Bamberg with the Chair for AI Systems Engineering.

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"

Any setting may be overridden for a single call:

AtpClient.Isabelle.query(theory, "Example", session: "Main", raw: true)