Modules
Elixir client for external automated theorem provers.
Behaviour every backend implements so a UI (Smart Cell, Livebook, …) can discover its configurable settings and probe reachability without hard-coding per-backend knowledge.
Resolves configuration for each backend by merging (in increasing precedence)
One configurable setting on a backend, in a shape a UI can render directly.
Client for Isabelle servers, built on top of IsabelleClient from the
:isabelle_elixir package.
Handle for an open Isabelle server session.
Syntax and type diagnostics for TPTP input, aggregated across one or more backends.
One structured issue produced by an AtpClient.Lint backend.
Pure-Elixir structural checker for TPTP input.
The combined output of a lint pass: a list of Diagnostics and a list
of Symbols.
A symbol extracted from a TPTP source, currently always a declared
type coming from a type-role statement.
Authoritative TPTP syntax and type checker, delegated to TPTP4x on the SystemOnTPTP deployment.
Backend that invokes a locally installed, TPTP-compliant prover via
Port.open/2 and normalizes its stdout through
AtpClient.ResultNormalization.interpret_result/1.
Interprets output from various provers into SZS-faithful atoms.
Client for self-hosted StarExec instances.
An authenticated StarExec session.
Public tptp.org HTTP form API; see query_system/3 and query_all_systems/2.
Stateful Agent that caches the list of prover identifiers currently
advertised by a SystemOnTPTP deployment.