# Demo of the AtpClient Smart Cells

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

## Configuring a backend

Open the **ATP Backend Configuration** cell to wire each backend you intend to
use. The form is schema-driven — fields come straight from
`AtpClient.<Backend>.config_schema/0`, grouped into Connection / Defaults /
Advanced. Click **Verify connection** to call the backend's `verify/1` callback
before depending on its settings.

For Isabelle in particular: if the `isabelle` executable is on `PATH` (or
`ISABELLE_TOOL` is set), leave every field blank — the cell will auto-spawn a
local server and reuse one `HOL` session across solves. Fill in `host`, `port`,
`password`, etc. only when targeting a remote `isabelle server`.

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

```elixir
Application.put_env(:atp_client, :isabelle, [
  port: 17368,
  password: "a64c4ef5-bc6e-4714-a283-260e94c54a19",
  local_dir: "d:/Uni/26 SS/AtpClient/tmp",
  isabelle_dir: "/cygdrive/d/Uni/26 SS/AtpClient/tmp"
])

```

## SystemOnTPTP

`SystemOnTPTP` needs no credentials — the cell ships ready to pick a prover
from the live-fetched list and run it.

```elixir
server_info = [
  host: "127.0.0.1",
  port: 17368,
  password: "a64c4ef5-bc6e-4714-a283-260e94c54a19",
  local_dir: "d:/Uni/26 SS/AtpClient/tmp",
  isabelle_dir: "/cygdrive/d/Uni/26 SS/AtpClient/tmp"
]

theory = """
thf(test, conjecture, ![P:$o]: (P => ~P)).
thf(test, conjecture, ![P:$o]: (P => P)).
"""
```

```elixir
IsabelleClient.TPTP.isabellize_theory(theory)
```

```elixir
theory
|> IsabelleClient.TPTP.isabellize_theory
# |> String.trim
# |> String.replace("\n\n", "\n")
# |> String.split("\n")
# |> Enum.map(& "#{&1} by auto")
# |> Enum.join("\n")
|> AtpClient.Isabelle.query_lemmas("Example", [proof_method: "nitpick"] ++ server_info)
```

<!-- livebook:{"attrs":"eyJiYWNrZW5kIjoiaXNhYmVsbGUiLCJwcm9ibGVtX3N0ciI6InRoZihhLCBjb25qZWN0dXJlLCAhW1A6JG9dOiAoUCA9PiB+UCkpLlxyXG50aGYoYiwgY29uamVjdHVyZSwgIVtQOiRvXTogKFAgPT4gUCkpLiIsInByb29mX21ldGhvZCI6ImJ5IGF1dG8iLCJzeXN0ZW0iOiJBbHQtRXJnby0tLTAuOTUuMiIsInRoZW1lIjoiRHJhY3VsYSIsInRpbWVfbGltaXQiOjUsInRwdHA0eF9lbmFibGVkIjpmYWxzZX0","chunks":null,"kind":"Elixir.KinoAtpClient.AtpSolver","livebook_object":"smart_cell"} -->

```elixir
# Generated by ATP Solver (backend: Isabelle)
problem = "thf(a, conjecture, ![P:$o]: (P => ~P)).\r\nthf(b, conjecture, ![P:$o]: (P => P))."

# Uses the auto-managed local Isabelle server when `isabelle` is on PATH,
# otherwise falls back to AtpClient.Isabelle's remote-config path.
case KinoAtpClient.IsabelleRuntime.available?() do
  :ok -> KinoAtpClient.IsabelleRuntime.query_tptp(problem, proof_method: "by auto")
  {:error, _} -> AtpClient.Isabelle.query_tptp(problem, proof_method: "by auto")
end

```

## Isabelle (zero-config)

With a local `isabelle` on `PATH`, the same TPTP problem runs against the
auto-managed session. Switching the backend dropdown to `Isabelle` swaps the
header controls (proof method picker) and the result panel (per-lemma table).

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

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

```

## Other backends

Switch the backend dropdown to `StarExec` or `LocalExec` to run against a
self-hosted StarExec deployment or a locally installed TPTP-compliant prover
(E, Vampire, …). Both normalize their output to a single SZS-status badge.