AtpClient

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

• SystemOnTPTP — the public tptp.org HTTP form endpoint.
• StarExec — self-hosted StarExec deployments.
• Isabelle — isabelle server instances, via the isabelle_elixir package.

All backends return results normalized to AtpClient.ResultNormalization.atp_result so that comparing provers across backends is straightforward and can be used in downstream tasks.

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

Installation

Add :atp_client to your dependencies in mix.exs:

def deps do
  [
    {:atp_client, "~> 0.1"}
  ]
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"

Any setting may be overridden for a single call:

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

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", "cvc5---1.3.0", ...]

AtpClient.SystemOnTptp.query_system(problem, "cvc5---1.3.0", time_limit_sec: 10)
# => {:ok, :thm}

AtpClient.SystemOnTptp.query_selected_systems(problem, ["cvc5---1.3.0", "Vampire---5.0"], time_limit_sec: 5)
# => {:ok, [{"cvc5---1.3.0", {:ok, :thm}}, {"Vampire---5.0", {:ok, :thm}}]}

AtpClient.SystemOnTptp.query_all_systems(problem, time_limit_sec: 5)
# => {:ok, [{"Alt-Ergo---0.95.3", {:ok, :thm}}, ...]}

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 ids come from `info`; stdout is then normalized the same way as
# SystemOnTPTP output:
{:ok, stdout} = AtpClient.StarExec.get_pair_stdout(session, pair_id)
AtpClient.ResultNormalization.interpret_result(stdout)
# => {:ok, :thm}

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

theory = ~S"""
theory Example imports Main
begin

lemma "\<forall>x. P x \<longrightarrow> P x"
  by auto

end
"""

# The first result in the output is interpreted. "Successful" tool calls, e.g.
# finding a proof or countermodel, take precedence. Multiple formulae are not
# supported.
AtpClient.Isabelle.query(theory, "Example")
# => {:ok, {:ok, :thm}}

# With an existing session, reuse the socket for multiple theories:
{:ok, session} = AtpClient.Isabelle.open_session()
AtpClient.Isabelle.prove_theory(session, theory, "Example")
AtpClient.Isabelle.prove_theory(session, other_theory, "Example2")
AtpClient.Isabelle.close_session(session)

# Pass `raw: true` to inspect the full Isabelle status list instead:
{:ok, status} = AtpClient.Isabelle.query(theory, "Example", raw: true)
AtpClient.ResultNormalization.extract_isabelle_text(status)
# => "...\nSledgehammering...\nverit found a proof...\n..."

License

MIT.