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

The SZS ontologies: their 112 status values, the 3 ontologies
the values belong to, and the `isa` hierarchy among them.

DO NOT EDIT. Generated by `mix tptp.gen` from
`priv/bnf/SZSOntology.bnf`.

Each value is a nonterminal of the BNF, and its rule names the value's own
terminal and the values directly beneath it:

    <Theorem> ::= Theorem | <SatisfiableAxiomsTheorem> | <ContradictoryAxioms>

Here `children(:theorem)` is `[:satisfiable_axioms_theorem, :contradictory_axioms]`,
and `:theorem` is among the `parents/1` of each. The hierarchy is
a directed acyclic graph rather than a tree: `<Theorem>` itself has
3 parents,
`<SatisfiabilityPreserving>`, `<TautologyPreserving>`, `<FiniteTheorem>`.
`ancestors/1` and `descendants/1` are the transitive closures, and `isa?/2` is
the derivability of one value's terminal from another value's nonterminal.

The ontologies are the alternatives of `<SZS>`:
`<Success>`, `<NoSuccess>`, `<Data>`. Every value sits beneath exactly
one of them, and `ontology/1` says which.

One terminal takes arguments: `<Assumed> ::= Assumed(<Unknown>,<Success>)`.
The references inside the parentheses are the domains of the arguments and not
`isa` edges; `arguments/1` lists them.

Every atom is created at compile time, so `from_string/1` converts untrusted
prover output to an atom without `String.to_atom/1` being reachable from
input. See `Tptp.Token` for the same constraint and the Credo check enforcing
it.

The BNF carries neither mnemonics nor descriptions. `Tptp.Szs.Page`
transcribes those from the ontology page by hand, and the functions here that
answer with them delegate to it.

# `ontology`

```elixir
@type ontology() :: :success | :no_success | :data
```

Which of the 3 SZS ontologies a value belongs to: the alternatives of `<SZS>`.

# `t`

```elixir
@type t() ::
  :success
  | :semantic_success
  | :unsatisfiability_preserving
  | :satisfiability_preserving
  | :tautology_preserving
  | :equi_satisfiable
  | :equi_tautologous
  | :satisfiable
  | :finitely_satisfiable
  | :theorem
  | :finite_theorem
  | :satisfiable_axioms_theorem
  | :equivalent
  | :tautologous_conclusion
  | :weaker_conclusion
  | :equivalent_theorem
  | :tautology
  | :finite_tautology
  | :weaker_tautologous_conclusion
  | :weaker_theorem
  | :model_extending
  | :no_consequence
  | :contradictory_axioms
  | :satisfiable_conclusion_contradictory_axioms
  | :tautologous_conclusion_contradictory_axioms
  | :weaker_conclusion_contradictory_axioms
  | :counter_unsatisfiability_preserving
  | :counter_satisfiability_preserving
  | :counter_tautology_preserving
  | :equi_counter_satisfiable
  | :equi_counter_tautologous
  | :counter_satisfiable
  | :finitely_counter_satisfiable
  | :counter_theorem
  | :finite_counter_theorem
  | :satisfiable_axioms_counter_theorem
  | :counter_equivalent
  | :unsatisfiable_conclusion
  | :weaker_counter_conclusion
  | :equivalent_counter_theorem
  | :unsatisfiable
  | :finitely_unsatisfiable
  | :weaker_unsatisfiable_conclusion
  | :weaker_counter_theorem
  | :counter_model_extending
  | :satisfiable_counter_conclusion_contradictory_axioms
  | :unsatisfiable_conclusion_contradictory_axioms
  | :type_check_success
  | :type_check_partial
  | :type_checked_complete
  | :verify_success
  | :verified_good
  | :verified_bad
  | :no_success
  | :unknown
  | :stopped
  | :in_progress
  | :not_tried
  | :not_tried_yet
  | :error
  | :forced
  | :gave_up
  | :os_error
  | :input_error
  | :syntax_error
  | :semantic_error
  | :type_error
  | :unsemantic
  | :usage_error
  | :user
  | :resource_out
  | :timeout
  | :cpu_timeout
  | :wc_timeout
  | :memory_out
  | :incomplete
  | :inappropriate
  | :incorrect
  | :assumed
  | :open
  | :not_verified
  | :failed_verified
  | :data
  | :logical_data
  | :non_logical_data
  | :not_a_solution
  | :solution
  | :assurance
  | :incomplete_proof
  | :incomplete_interpretation
  | :proof
  | :interpretation
  | :list_of_formulae
  | :refutation
  | :derivation
  | :cnf_refutation
  | :model
  | :domain_interpretation
  | :domain_model
  | :finite_interpretation
  | :finite_model
  | :infinite_interpretation
  | :infinite_model
  | :herbrand_interpretation
  | :herbrand_model
  | :formula_herbrand_interpretation
  | :formula_herbrand_model
  | :saturation
  | :comment
  | :free_text
  | :verification
  | :none
```

One SZS status value. A closed set of 112 compile-time atoms.

# `ancestors`

```elixir
@spec ancestors(t()) :: [t()]
```

Every value above a value, in the order the BNF defines them. The value itself
is not among them.

    iex> Tptp.Szs.Ontology.ancestors(:equivalent_theorem)
    [:success, :semantic_success, :unsatisfiability_preserving, :satisfiability_preserving, :tautology_preserving, :equi_satisfiable, :equi_tautologous, :satisfiable, :theorem, :finite_theorem, :satisfiable_axioms_theorem, :equivalent, :model_extending, :counter_unsatisfiability_preserving, :counter_satisfiability_preserving, :counter_tautology_preserving, :equi_counter_satisfiable, :equi_counter_tautologous]

# `arguments`

```elixir
@spec arguments(t()) :: [t()]
```

The values a terminal takes as arguments, or `[]` for the terminals that take none.

    iex> Tptp.Szs.Ontology.arguments(:assumed)
    [:unknown, :success]
    iex> Tptp.Szs.Ontology.arguments(:theorem)
    []

# `children`

```elixir
@spec children(t()) :: [t()]
```

The values directly beneath a value: the nonterminals its rule lists, in that order.

    iex> Tptp.Szs.Ontology.children(:theorem)
    [:satisfiable_axioms_theorem, :contradictory_axioms]
    iex> Tptp.Szs.Ontology.children(:tautology)
    []

# `count`

```elixir
@spec count() :: pos_integer()
```

How many status values there are.

# `data?`

```elixir
@spec data?(t()) :: boolean()
```

Whether a value describes a form of data rather than a result.

    iex> Tptp.Szs.Ontology.data?(:cnf_refutation)
    true

# `descendants`

```elixir
@spec descendants(t()) :: [t()]
```

Every value beneath a value, in the order the BNF defines them. The value itself
is not among them.

    iex> Tptp.Szs.Ontology.descendants(:type_check_success)
    [:type_check_partial, :type_checked_complete]

# `describe`

```elixir
@spec describe(t()) :: binary()
```

What the page says a status value means. See `Tptp.Szs.Page.describe/1`.

# `from_mnemonic`

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

Turn a mnemonic into an atom. See `Tptp.Szs.Page.from_mnemonic/1`.

# `from_status_value`

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

Turn a `status(...)` mnemonic into an atom. See `Tptp.Szs.Page.from_status_value/1`.

# `from_string`

```elixir
@spec from_string(binary()) :: {:ok, t()} | :error
```

Turn a `OneWord` status value into an atom, without creating one.

    iex> Tptp.Szs.Ontology.from_string("Theorem")
    {:ok, :theorem}
    iex> Tptp.Szs.Ontology.from_string("NotAStatus")
    :error

# `isa?`

```elixir
@spec isa?(t(), t()) :: boolean()
```

Whether `value` is `other` or sits beneath it: whether the BNF derives
`value`'s terminal from `<other>`.

    iex> Tptp.Szs.Ontology.isa?(:theorem, :satisfiable)
    false
    iex> Tptp.Szs.Ontology.isa?(:equivalent_theorem, :satisfiable)
    true
    iex> Tptp.Szs.Ontology.isa?(:theorem, :theorem)
    true

# `mnemonic`

```elixir
@spec mnemonic(t()) :: binary()
```

The three-letter mnemonic for a status value. See `Tptp.Szs.Page.mnemonic/1`.

# `name`

```elixir
@spec name(t()) :: binary()
```

The `OneWord` spelling of a status value: its nonterminal's name.

    iex> Tptp.Szs.Ontology.name(:counter_satisfiable)
    "CounterSatisfiable"

# `no_success?`

```elixir
@spec no_success?(t()) :: boolean()
```

Whether a value says why nothing was established.

    iex> Tptp.Szs.Ontology.no_success?(:timeout)
    true

# `ontologies`

```elixir
@spec ontologies() :: [ontology()]
```

The 3 ontologies, as `<SZS>` lists them.

# `ontology`

```elixir
@spec ontology(t()) :: ontology()
```

Which of the 3 ontologies a value belongs to: the root it descends from.

    iex> Tptp.Szs.Ontology.ontology(:theorem)
    :success
    iex> Tptp.Szs.Ontology.ontology(:timeout)
    :no_success

# `parents`

```elixir
@spec parents(t()) :: [t()]
```

The values a value sits directly beneath, in the order the BNF defines them.

    iex> Tptp.Szs.Ontology.parents(:theorem)
    [:satisfiability_preserving, :tautology_preserving, :finite_theorem]
    iex> Tptp.Szs.Ontology.parents(:success)
    []

# `source`

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

The BNF these values are generated from.

The file carries no version number; `NOTICE` records the commit it was taken at.

# `success?`

```elixir
@spec success?(t()) :: boolean()
```

Whether a value says something was established.

    iex> Tptp.Szs.Ontology.success?(:theorem)
    true
    iex> Tptp.Szs.Ontology.success?(:gave_up)
    false

# `value?`

```elixir
@spec value?(term()) :: boolean()
```

Whether a term is a status value at all.

    iex> Tptp.Szs.Ontology.value?(:theorem)
    true
    iex> Tptp.Szs.Ontology.value?(:banana)
    false

# `values`

```elixir
@spec values() :: [t()]
```

Every status value, in the order the BNF defines them.

---

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