atp_client

# Elixir meets TPTP — PAAR'26 talk demo

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

## Setup

```elixir
alias AtpClient.{SystemOnTptp, Isabelle, LocalExec}
```

```elixir
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---")
}
```

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

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

```elixir
LocalExec.verify(binary: "eprover")
```

---

<!-- livebook:{"branch_parent_index":0} -->

## A. Uniform result type

<!--
 Speaker cue: "This is slide 7 running. Same problem, three transport
     mechanisms, one result shape." 
-->

The problem: **functional extensionality**, stated in THF.

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

**Remote prover on SystemOnTPTP:**

```elixir
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):

```elixir
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:

```elixir
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.**

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

```elixir
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
)
```

---

<!-- livebook:{"branch_parent_index":0} -->

## B. Portfolio solving

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

```elixir
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))
```

---

<!-- livebook:{"branch_parent_index":0} -->

## C. The Smart Cell: TPTP front-end

<!--
 Speaker cue: "Everything so far was the library. This is the first
     downstream consumer — no backend-specific code in it."

     LIVE SCRIPT for this beat (the typing IS the demo):
     1. Add a new ATP Solver smart cell fresh (⌘/Ctrl-click "+ Smart" →
        ATP Solver) — or reuse the pre-seeded one below as fallback.
     2. Type a small problem. Deliberately mistype a role first:
        `thf(oops, conjectur, $true).` → the two-tier linter underlines the
        unknown role inline (Monaco marker). Fix it.
     3. Hover `$i` or `!` → the explanatory card ("valuable for novices").
     4. One-click Solve on SystemOnTPTP.
     5. Flip the backend dropdown to Isabelle → controls swap to the proof
        method picker; solve again → per-lemma result table.
     "Zero Elixir written. And the cell generated the Elixir it represents —
     look at the code it left behind." 
-->

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):

<!-- livebook:{"attrs":"eyJiYWNrZW5kIjoic3RhcmV4ZWMiLCJ2YWx1ZXMiOnt9fQ","chunks":null,"kind":"Elixir.KinoAtpClient.BackendConfig","livebook_object":"smart_cell"} -->

```elixir
# 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):

<!-- livebook:{"attrs":"eyJiYWNrZW5kIjoic3RhcmV4ZWMiLCJwcm9ibGVtX3N0ciI6InRoZihleHQsIGNvbmplY3R1cmUsXHJcbiAgICAhW0Y6JGk+JGksIEc6JGk+JGldOiAoKCFbWDokaV06ICgoRiBAIFgpID0gKEcgQCBYKSkpID0+IChGID0gRykpXHJcbikuIiwicHJvb2ZfbWV0aG9kIjoidHJ5IG9vcHMiLCJzeXN0ZW0iOiJjdmM1LS0tMS4zLjQiLCJ0aGVtZSI6IkRyYWN1bGEiLCJ0aW1lX2xpbWl0Ijo1LCJ0cHRwNHhfZW5hYmxlZCI6ZmFsc2V9","chunks":null,"kind":"Elixir.KinoAtpClient.AtpSolver","livebook_object":"smart_cell"} -->

```elixir
# 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)

```

---

<!-- livebook:{"branch_parent_index":0} -->

## Teardown

```elixir
IsabelleClient.Server.kill(server.name)
```