Demo of the AtpClient Smart Cells

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.

Application.put_env(:atp_client, :isabelle, [
  port: 44155,
  password: "a8c4b49b-79e3-4dd6-ab7e-8404d8422b69",
  local_dir: "d:/Uni/26 SS/KinoAtpClient/tmp",
  isabelle_dir: "/cygdrive/d/Uni/26 SS/KinoAtpClient/tmp"
])

Application.put_env(:atp_client, :local_exec, [binary: "d:\\Uni\\26 SS\\AtpClient\\priv\\bin\\eprover"])

SystemOnTPTP

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

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

# 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: "try oops")
  {:error, _} -> AtpClient.Isabelle.query_tptp(problem, proof_method: "try oops")
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).

# Generated by ATP Solver (backend: Isabelle)
problem = "thf(test, conjecture, $true => $true)."

# 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

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.

← Previous Page KinoAtpClient