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.
Summary
Types
Which of the 3 SZS ontologies a value belongs to: the alternatives of <SZS>.
One SZS status value. A closed set of 112 compile-time atoms.
Functions
Every value above a value, in the order the BNF defines them. The value itself is not among them.
The values a terminal takes as arguments, or [] for the terminals that take none.
The values directly beneath a value: the nonterminals its rule lists, in that order.
How many status values there are.
Whether a value describes a form of data rather than a result.
Every value beneath a value, in the order the BNF defines them. The value itself is not among them.
What the page says a status value means. See Tptp.Szs.Page.describe/1.
Turn a mnemonic into an atom. See Tptp.Szs.Page.from_mnemonic/1.
Turn a status(...) mnemonic into an atom. See Tptp.Szs.Page.from_status_value/1.
Turn a OneWord status value into an atom, without creating one.
Whether value is other or sits beneath it: whether the BNF derives
value's terminal from <other>.
The three-letter mnemonic for a status value. See Tptp.Szs.Page.mnemonic/1.
The OneWord spelling of a status value: its nonterminal's name.
Whether a value says why nothing was established.
The 3 ontologies, as <SZS> lists them.
Which of the 3 ontologies a value belongs to: the root it descends from.
The values a value sits directly beneath, in the order the BNF defines them.
The BNF these values are generated from.
Whether a value says something was established.
Whether a term is a status value at all.
Every status value, in the order the BNF defines them.
Types
@type ontology() :: :success | :no_success | :data
Which of the 3 SZS ontologies a value belongs to: the alternatives of <SZS>.
@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.
Functions
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]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)
[]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)
[]@spec count() :: pos_integer()
How many status values there are.
Whether a value describes a form of data rather than a result.
iex> Tptp.Szs.Ontology.data?(:cnf_refutation)
trueEvery 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]What the page says a status value means. See Tptp.Szs.Page.describe/1.
Turn a mnemonic into an atom. See Tptp.Szs.Page.from_mnemonic/1.
Turn a status(...) mnemonic into an atom. See Tptp.Szs.Page.from_status_value/1.
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")
:errorWhether 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)
trueThe three-letter mnemonic for a status value. See Tptp.Szs.Page.mnemonic/1.
The OneWord spelling of a status value: its nonterminal's name.
iex> Tptp.Szs.Ontology.name(:counter_satisfiable)
"CounterSatisfiable"Whether a value says why nothing was established.
iex> Tptp.Szs.Ontology.no_success?(:timeout)
true@spec ontologies() :: [ontology()]
The 3 ontologies, as <SZS> lists them.
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_successThe 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)
[]@spec source() :: binary()
The BNF these values are generated from.
The file carries no version number; NOTICE records the commit it was taken at.
Whether a value says something was established.
iex> Tptp.Szs.Ontology.success?(:theorem)
true
iex> Tptp.Szs.Ontology.success?(:gave_up)
falseWhether a term is a status value at all.
iex> Tptp.Szs.Ontology.value?(:theorem)
true
iex> Tptp.Szs.Ontology.value?(:banana)
false@spec values() :: [t()]
Every status value, in the order the BNF defines them.