# AtpClient v0.5.0 - Table of Contents

> Elixir client for automated theorem provers via SystemOnTPTP, StarExec, and Isabelle servers.

## Pages

- [AtpClient](readme.md)
- [Changelog](changelog.md)

- Examples
  - [Demo of the AtpClient Package](demo.md)
  - [Isabelle TPTP smoke test](isabelle_tptp.md)

## Modules

- [AtpClient](AtpClient.md): Elixir client for external automated theorem provers.

- Backend integrations
  - [AtpClient.Backend](AtpClient.Backend.md): Behaviour every backend implements so a UI (Smart Cell, Livebook, …) can
discover its configurable settings and probe reachability without
hard-coding per-backend knowledge.
  - [AtpClient.Isabelle](AtpClient.Isabelle.md): Client for Isabelle servers, built on top of `IsabelleClient` from the
`:isabelle_elixir` package.
  - [AtpClient.Isabelle.Session](AtpClient.Isabelle.Session.md): Handle for an open Isabelle server session.
  - [AtpClient.LocalExec](AtpClient.LocalExec.md): Backend that invokes a locally installed, TPTP-compliant prover via
`Port.open/2` and normalizes its stdout through
`AtpClient.ResultNormalization.interpret_result/1`.
  - [AtpClient.StarExec](AtpClient.StarExec.md): Client for self-hosted StarExec instances.
  - [AtpClient.StarExec.Session](AtpClient.StarExec.Session.md): An authenticated StarExec session.
  - [AtpClient.SystemOnTptp](AtpClient.SystemOnTptp.md): Public tptp.org HTTP form API; see `query_system/3` and `query_all_systems/2`.
  - [AtpClient.SystemOnTptp.Provers](AtpClient.SystemOnTptp.Provers.md): Stateful `Agent` that caches the list of prover identifiers currently
advertised by a SystemOnTPTP deployment.

- Lint
  - [AtpClient.Lint](AtpClient.Lint.md): Syntax and type diagnostics for TPTP input, aggregated across one or
more backends.
  - [AtpClient.Lint.Diagnostic](AtpClient.Lint.Diagnostic.md): One structured issue produced by an `AtpClient.Lint` backend.
  - [AtpClient.Lint.Local](AtpClient.Lint.Local.md): Pure-Elixir structural checker for TPTP input.
  - [AtpClient.Lint.Report](AtpClient.Lint.Report.md): The combined output of a lint pass: a list of `Diagnostic`s and a list
of `Symbol`s.
  - [AtpClient.Lint.Symbol](AtpClient.Lint.Symbol.md): A symbol extracted from a TPTP source, currently always a declared
type coming from a `type`-role statement.
  - [AtpClient.Lint.Tptp4x](AtpClient.Lint.Tptp4x.md): Authoritative TPTP syntax and type checker, delegated to TPTP4x on the
SystemOnTPTP deployment.

- Support
  - [AtpClient.Config](AtpClient.Config.md): Resolves configuration for each backend by merging (in increasing precedence)
  - [AtpClient.Config.Field](AtpClient.Config.Field.md): One configurable setting on a backend, in a shape a UI can render directly.
  - [AtpClient.ResultNormalization](AtpClient.ResultNormalization.md): Interprets output from various provers into SZS-faithful atoms.