# AtpClient v0.7.2 - Table of Contents

> Elixir client for automated theorem provers via SystemOnTPTP, StarExec, Isabelle servers and local binaries, on the tptp library.

## Pages

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

- Examples
  - [AtpClient — end-to-end demo](demo.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): Opaque 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 reads its stdout through `AtpClient.Verdict`.
  - [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 system identifiers currently advertised by
a SystemOnTPTP deployment.

- Problems and results
  - [AtpClient.Isabelle.Verdict](AtpClient.Isabelle.Verdict.md): Reads the `use_theories` payload of an Isabelle server into SZS values.
  - [AtpClient.Problem](AtpClient.Problem.md): What a backend accepts as the problem to prove.
  - [AtpClient.Result](AtpClient.Result.md): What a backend returns when the system it ran asserted a result.
  - [AtpClient.Verdict](AtpClient.Verdict.md): Reads a system's output into an `AtpClient.Result`.

- Analyzers
  - [AtpClient.Analyzer.Tptp4x](AtpClient.Analyzer.Tptp4x.md): TPTP4X as a `Tptp.Analyzer`: syntax and type findings from the TPTP World's own
checker, run on the configured 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.

