# `Tptp.Szs.Page`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/szs/page.ex#L1)

What <https://szs.tptp.org> says about the SZS values and the BNF does not:
their mnemonics and their descriptions.

This module is written by hand and maintained by hand. `Tptp.Szs.Ontology` is
generated from the vendored `SZSOntology.bnf`, which is the TPTP World's source
of truth for the values and the `isa` hierarchy among them, and delegates to this
module for everything else. The page publishes the mnemonics and descriptions in
prose only, so they are transcribed here and edited when the page changes; the
test suite checks that every generated value has both, so a value added to the
BNF fails the build until its entry is transcribed.

Each value's `describe/1` text is quoted from the page. `NOTICE` carries the
attribution the TPTP's terms require for it.

## Case sensitivity

`SAT` is `Satisfiable` and `Sat` is `Saturation`, so `from_mnemonic/1` is case
sensitive. The lower-case three-letter form occurring inside a TPTP
`status(...)` annotation has a separate entry point, `from_status_value/1`,
which searches the success ontology alone, that being the only source
`<inference_status_value>` draws from, as the test suite verifies against the BNF.

`Ass` and `ASS` are a second such pair: `Ass` is `Assurance` in the data
ontology and `ASS` is `Assumed` in the no-success ontology.

## Arguments of `Assumed`

Every mnemonic on the page is three letters except one. `Assumed` is
`ASS(U,S)`: the success value `S` was assumed because the actual result is
unknown for the no-success reason `U`, where `U` is drawn from the subontology
beneath `Unknown`. The BNF states the same as
`<Assumed> ::= Assumed(<Unknown>,<Success>)`, and
`Tptp.Szs.Ontology.arguments/1` reports the two domains. `mnemonic(:assumed)`
returns `"ASS"` and `from_mnemonic/1` accepts `"ASS"` alone, since a pair of
arguments is not a member of a closed set of atoms.

A consumer reading such a status line must decompose it: take the text
preceding the first `(`, resolve it here, and resolve the two arguments, which
are themselves mnemonics, with further calls. The page does not state how the
form is written in a `% SZS status` line, and the TPTP BNF cannot express it:
`<status_value>` is a list of plain words, so `status(ass(...))` has no
derivation. Treat `ASS(...)` as a form to recognise rather than to emit.

# `describe`

```elixir
@spec describe(Tptp.Szs.Ontology.t()) :: binary()
```

What the page says a status value means, in its own words.

    iex> Tptp.Szs.Page.describe(:theorem)
    "All models of Ax are models of C."

# `from_mnemonic`

```elixir
@spec from_mnemonic(binary()) ::
  {:ok, Tptp.Szs.Ontology.t()} | {:ambiguous, [Tptp.Szs.Ontology.t()]} | :error
```

Turn a three-letter mnemonic into an atom. Case sensitive, because case is
meaningful: `SAT` is `Satisfiable` and `Sat` is `Saturation`.

A mnemonic the page reuses answers `{:ambiguous, values}` rather than picking
one — `IIn` is both `InfiniteInterpretation` and `IncompleteInterpretation`.

    iex> Tptp.Szs.Page.from_mnemonic("THM")
    {:ok, :theorem}
    iex> Tptp.Szs.Page.from_mnemonic("IIn")
    {:ambiguous, [:infinite_interpretation, :incomplete_interpretation]}
    iex> Tptp.Szs.Page.from_mnemonic("thm")
    :error

# `from_status_value`

```elixir
@spec from_status_value(binary()) :: {:ok, Tptp.Szs.Ontology.t()} | :error
```

Turn the lower-case mnemonic inside a TPTP `status(...)` annotation into an atom.

`<inference_status_value>` in the SZS BNF is the success ontology's mnemonic,
lower-cased, and the test suite checks that all of them are present here.

    iex> Tptp.Szs.Page.from_status_value("thm")
    {:ok, :theorem}
    iex> Tptp.Szs.Page.from_status_value("prf")
    :error

# `mnemonic`

```elixir
@spec mnemonic(Tptp.Szs.Ontology.t()) :: binary()
```

The three-letter mnemonic for a status value.

    iex> Tptp.Szs.Page.mnemonic(:theorem)
    "THM"

# `source`

```elixir
@spec source() :: binary()
```

The page these mnemonics and descriptions are transcribed from.

The page carries no version number, so there is nothing finer to report. The
transcription was last checked against it on 2026-09-10.

---

*Consult [api-reference.md](api-reference.md) for complete listing*