Powered by AppSignal & Oban Pro
Notesclub
Sign in with GitHub
created by hec & contributors
terms privacy

Elixir meets TPTP — PAAR'26 demo

examples/demo.livemd

avatar
Johannes Schuster
avatar
avatar
Share to X
Share to Bluesky
More notebooks

Elixir meets TPTP — PAAR’26 demo

Mix.install([
  # automatically loads atp_client and kino as transitive dependencies as well
  {:kino_atp_client, "~> 0.6"}
])

Setup (not part of the demonstration)

Imports of the implemented backends:

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

Fix prover selection for reproducibility (don’t pin versions):

pick_prover = fn prefix ->
  SystemOnTptp.list_provers()
  |> Enum.find(&String.starts_with?(&1, prefix))
end

provers = %{
  leo3: pick_prover.("Leo-III---"),
  cvc5: pick_prover.("cvc5---"),
  vampire: pick_prover.("Vampire---"),
  zipperposition: pick_prover.("Zipperpin---")
}

Start an isabelle server (the isabelle executable must be on the PATH for that or ISABELLE_TOOL be set) :

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

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

Verify that the eprover-ho binary is executable from this environment:

LocalExec.verify(binary: "eprover-ho")

Verify that the locally hosted StarExec server is reachable:

starexec_opts = [
  base_url: "https://127.0.0.1:7827",
  username: "admin",
  password: "admin",
  connect_options: [transport_opts: [verify: :verify_none]]
]

with {:ok, session} <- StarExec.login(starexec_opts) do
  StarExec.logout(session)
end

A. Uniform result type

Example problem: functional extensionality, stated in THF.

$\textrm{funExt} \coloneqq \forall F{\iota\to\iota} G{\iota\to\iota}.\,(\forall X_\iota.\, F~X = G~X) \supset F = G$

problem = """
thf(funExt, conjecture,
    ![F:$i>$i, G:$i>$i]: (
      (![X:$i]: (
        (F @ X) = (G @ X)
      ))
      =>
      (F = G)
    )
).
"""

IO.puts problem

Shorthand prover access defined in a setup cell:

provers

Remote prover on SystemOnTPTP:

SystemOnTptp.query_system(problem, provers.leo3, time_limit_sec: 10)

Querying multiple remote systems via one request:

with {:ok, res} <- SystemOnTptp.query_selected_systems(
  problem,
  [provers.zipperposition, provers.vampire],
  time_limit_sec: 10
) do
  res |> Enum.each(fn {sys, verdict} -> IO.inspect(verdict, label: sys) end)
end

Same TPTP problem, different backend: Isabelle/HOL. query_tptp/2 isabellizes the annotated formulae and returns one verdict per conjecture:

tptp_two_goals = problem <> """
thf(p_type, type, p: $i > $o).
thf(simpleCsat, conjecture, ![X: $i]: ((p @ X) & ~ (p @ X))).
"""

with {:ok, res} <- Isabelle.query_tptp(
  tptp_two_goals,
  isa_opts ++ [
    proof_method: "sledgehammer nitpick oops",
    use_theories_timeout_ms: 60_000
  ]
) do
  res |> Enum.each(&IO.inspect &1.result, label: &1.name)
end

One-line backend swap: a local binary, no network.

Application.put_env(:atp_client, :starexec,
  base_url: "https://127.0.0.1:7827",
  username: "admin",
  password: "admin",
  connect_options: [transport_opts: [verify: :verify_none]]
)

StarExec.query(problem,
  space_id: 1, solver_cfg_id: 1    # eprover-ho running on a self-hosted instance
)
LocalExec.query(problem,
  binary: "eprover-ho",
  args: ~w(--tstp-format --cpu-limit=10),
  cpu_timeout_s: 10
)

Setting raw: true allows us to inspect the prover’s uninterpreted output:

with {:ok, res} <- LocalExec.query(problem,
  binary: "eprover-ho",
  args: ~w(--tstp-format --cpu-limit=10),
  raw: true
) do
  IO.puts res
end

B. Portfolio solving

A harder problem: injective formulation of Cantor’s theorem.

$\neg\exists H{(\iota\to o)\to\iota}.\,\forall P{\iota\to o} Q_{\iota\to o}. (H~P = H~Q) \supset P = Q$

problem = """
thf(injCantor, conjecture,
  ~?[H:($i>$o)>$i]: (
    ![P:$i>$o, Q:$i>$o]: (
      ((H @ P) = (H @ Q))
      =>
      (P = Q)
    )
  )
).
"""

IO.puts problem

Watch the results stream in as provers finish. Stragglers are killed at the deadline without touching their peers:

frame = Kino.Frame.new() |> Kino.render()      # Front-end library for dynamic output

portfolio = [provers.leo3, provers.cvc5, provers.zipperposition, provers.vampire]

t0 = System.monotonic_time(:millisecond)

results =
  portfolio
  |> Task.async_stream(
    fn sys -> {sys, SystemOnTptp.query_system(problem, sys)} end,
    timeout: 5_000, on_timeout: :kill_task,    # kill stragglers after 5s
    ordered: false                             # non-deterministic scheduling
  )
  |> Enum.map(fn outcome ->
    dt = System.monotonic_time(:millisecond) - t0

    line =
      case outcome do
        {:ok, {sys, result}} -> "#{sys} ==> #{inspect(result)} (#{dt} ms)"
        {:exit, :timeout} -> "straggler killed at deadline (#{dt} ms)"
      end

    Kino.Frame.append(frame, Kino.Text.new(line))
    outcome
  end)

Enum.find(results, &match?({:ok, {_sys, {:ok, :theorem}}}, &1))

C. The Smart Cell: TPTP front-end

The Backend Configuration cell (schema-driven — the form is generated by walking config_schema/0; with isabelle on PATH, leave Isabelle blank and it auto-spawns a server):

Application.put_env(:atp_client, :local_exec, [binary: "eprover-ho"])

Application.put_env(:atp_client, :starexec, [
  base_url: "https://127.0.0.1:7827",
  username: "admin",
  password: "admin",
  space_id: 1,
  solver_cfg_id: 1,
  connect_options: [transport_opts: [verify: :verify_none]]
])

Clicking + Smart below this cell lets us select the editor Smart Cell ATP solver.

Example problems:

  • $h~(h~\top = h~\bot) = h~\bot$ <!– thf(h_type, type, h:$o>$i). thf(conj, conjecture, (h @ ((h @ $true) = (h @ $false))) = (h @ $false) ). –>
  • $(\forall X.\,\exists Y.\,r~X~Y) \vdash (\exists F.\,\forall X.\,r~X~(F~X))$ <!– thf(r_type, type, r:$i>$i>$o). thf(ax1, axiom, ![X:$i]: (?[Y:$i]: (r @ X @ Y)) ). thf(conj, conjecture, ?[F:$i>$i]: (![X:$i]: (r @ X @ (F @ X))) ). –>

Teardown the Isabelle server

IsabelleClient.Server.kill(server.name)

Releases

AtpClient — use your favorite theorem prover

KinoAtpClient — notebook front-end with syntax highlighting

AtpMcp — ATP tools for LLM agents

Other notebooks:

Back