Elixir meets TPTP — PAAR’26 talk demo

Mix.install([
  {:kino_atp_client, "~> 0.6"}
])

Setup

alias AtpClient.{SystemOnTptp, Isabelle, LocalExec}

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 the Isabelle server now — session startup is the expensive part (seconds), and we want beat 1 to be instant:

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

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

Probe the local prover once so a missing binary surfaces here, not on stage:

LocalExec.verify(binary: "eprover")

A. Uniform result type

The problem: functional extensionality, stated in THF.

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

Remote prover on SystemOnTPTP:

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

A selected portfolio, one round-trip (provers that can’t handle higher-order are dropped from the result list):

SystemOnTptp.query_selected_systems(
  problem,
  [provers.cvc5, provers.zipperposition],
  time_limit_sec: 10
)

Same TPTP problem, different backend: Isabelle/HOL. query_tptp/2 isabellizes the annotated formulae and returns one verdict per conjecture — note the second goal is deliberately false, and the result type keeps :theorem and :counter_satisfiable distinct:

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

Isabelle.query_tptp(
  tptp_two_goals,
  isa_opts ++ [proof_method: "sledgehammer nitpick oops", use_theories_timeout_ms: 600_000]
)

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

LocalExec.query(problem,
  binary: "eprover",
  args: ["--auto", "--tstp-format", "--cpu-limit=10"],
  cpu_timeout_s: 10
)

fof_problem = ~S"""
fof(ax1, axiom, p).
fof(ax2, axiom, (p => q)).
fof(goal, conjecture, q).
"""

LocalExec.query(fof_problem,
  binary: "eprover",
  args: ["--auto", "--tstp-format", "--cpu-limit=10"],
  cpu_timeout_s: 10
)

B. Portfolio solving

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

frame = Kino.Frame.new() |> Kino.render()

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, time_limit_sec: 15)} end,
    max_concurrency: 16,
    timeout: 20_000,
    on_timeout: :kill_task
  )
  |> Enum.map(fn outcome ->
    dt = System.monotonic_time(:millisecond) - t0

    line =
      case outcome do
        {:ok, {sys, result}} -> "#{dt} ms — #{sys} → #{inspect(result)}"
        {:exit, :timeout} -> "#{dt} ms — straggler killed at deadline"
      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):

# ATP Backend Configuration: no values set yet.

Pre-seeded ATP Solver cell as fallback (prefer adding one fresh on stage — the typing and linting is the demo):

# Generated by ATP Solver (backend: StarExec)
problem = "thf(ext, conjecture,\r\n    ![F:$i>$i, G:$i>$i]: ((![X:$i]: ((F @ X) = (G @ X))) => (F = G))\r\n)."

AtpClient.StarExec.query(problem, cpu_timeout_s: 5)

Teardown

IsabelleClient.Server.kill(server.name)