# AtpClient v0.2.0 - Table of Contents

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

## Pages

- [AtpClient](readme.md)
- [Demo of the AtpClient Package](demo.md)

## Modules

- [AtpClient](AtpClient.md): Elixir client for external automated theorem provers.
- [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.
- [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.

- Backend integrations
  - [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.StarExec](AtpClient.StarExec.md): Client for self-hosted StarExec instances.
  - [AtpClient.StarExec.Session](AtpClient.StarExec.Session.md): An authenticated StarExec session.

- Support
  - [AtpClient.Config](AtpClient.Config.md): Resolves configuration for each backend by merging (in increasing precedence)
  - [AtpClient.ResultNormalization](AtpClient.ResultNormalization.md): Interprets output from various provers into a standardized format.