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., FX = GX) \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:

with :ok <- SystemOnTptp.verify() do
  SystemOnTptp.query_system(problem, provers.leo3, time_limit_sec: 10)
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

Although not yet polished, users can still use Isabelle code and inspect the system output:

isabelle_problem = """
lemma sym_trans_implies_refl:
  assumes "∀x y. R x y ⟶ R y x"
      and "∀x y z. R x y ∧ R y z ⟶ R x z"
    shows "∀x. R x x"
  nitpick
  oops
"""

with {:ok, session} <- Isabelle.open_session(isa_opts),
     {:ok, res} <- Isabelle.prove_theory(
       session,
       _theory_text=isabelle_problem,
       _theory_name="Example",
       raw: true
     )
do
  res |> IsabelleClient.Result.messages |> IO.puts
  AtpClient.Isabelle.close_session(session)
end

One-line backend swap: StarExec and a local binary.

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
)

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}. (HP = HQ) \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.

# Generated by ATP Solver (backend: SystemOnTPTP)
problem = "thf(test, conjecture, $true => $true)."
system = "Alt-Ergo---0.95.2"
time_limit = 5

case AtpClient.SystemOnTptp.query_system(problem, system, time_limit_sec: time_limit, raw: true) do
  {:ok, output} ->
    IO.puts(output)
    output

  {:error, reason} ->
    raise "SystemOnTPTP error: #{inspect(reason)}"
end

Example problems:

  • $h~(h~\top = h~\bot) = h~\bot$
  • $(\forall X.,\exists Y.,rXY) \vdash (\exists F.,\forall X.,rX(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