Mix.install([
{:kino_atp_client, "~> 0.5"}
])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.
Note that you will have to run the cell for the configuration to be applied.
# ATP Backend Configuration: no values set yet.
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: SystemOnTPTP)
problem = "thf(example, conjecture,\r\n ![X:$i, Y:$i]: ((X = Y) => (![F:$i>$i]: ((F @ X) = (F @ Y))))\r\n)."
system = "Zipperpin---2.1"
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
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(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: "try oops")
{:error, _} -> AtpClient.Isabelle.query_tptp(problem, proof_method: "try oops")
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.