The SZS status values, transcribed from https://szs.tptp.org.

This module is written by hand and maintained by hand. 112 values across three ontologies:

• :success — 53 values
• :no_success — 29 values
• :data — 30 values

Every atom is created at compile time, so from_string/1 and its counterparts convert untrusted prover output to an atom without String.to_atom/1 being reachable from input. This is a security property rather than a stylistic one; see Tptp.Token for the same constraint and the Credo check enforcing it.

Why this is not generated

The grammar is generated because the BNF is a formal document that changes with every TPTP release and is too large to transcribe reliably. The SZS ontology is neither. It is a prose page of 112 entries that has changed once in this library's lifetime — a doubled letter in one name — and scraping it cost a vendored copy of a Google Sites document, an HTML extractor written against that document's markup, and a generator, all to reproduce a table that can simply be written down. Amending an entry by hand when the page changes is less work than maintaining the machinery that reads it, and is reviewable in the diff.

What the machinery did enforce is kept as tests rather than lost: that every BNF <status_value> resolves here to a success-ontology mnemonic, that names and atoms round-trip, and that every value can be written and read back. See Tptp.SzsTest.

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

The isa hierarchy is not modelled

There is no parent/1 or descendant?/2. The SZS ontologies are hierarchies — EquivalentTheorem isa Equivalent isa Satisfiable — but the hierarchy is published only as three diagrams (Success.png, NoSuccess.png and Data.png at the URL above) and does not appear in the text of the page. Transcribing a diagram by inspection would introduce unverifiable relations into a library whose contract is fidelity to its sources. What is provided is the partition the text does state: the ontology a value belongs to, and its subontology within Success. Publication of a machine-readable ontology would allow the hierarchy to be added.

Ordering

There is no compare/2 and no precedence table, for the same reason: the page publishes none. A consumer comparing two prover results nonetheless requires a basis for the comparison, and an invented ranking admits precedence inversions, in which a Timeout from the longest-running system outranks a Theorem. Two published properties suffice:

• success?/1. A Success value constitutes an answer and a NoSuccess value its absence. Prefer Success. This is the whole of the ordering the text supports; no NoSuccess value is preferable to any Success value.
• subontology/1. Within Success, this identifies the group a value belongs to, allowing two answers to be compared as claims of the same or different kinds without assuming a strength ordering.

A further consideration concerns provenance. An explicit % SZS status line is the system's own statement of its conclusion, whereas an implementation-specific output pattern is an inference drawn by the reader. Prefer the line. Tptp.Szs.status/1 returns :none where a run emitted none, which is the condition under which a pattern may be used.

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 <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. 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.