- LogicalData (LDa): Logical data.
- Solution (Sol): A solution.
- Proof (Prf): A proof.
- Derivation (Der): A derivation (inference steps ending in the theorem, in the Hilbert style).
- Refutation (Ref): A refutation (starting with Ax ∪ ¬C and ending in FALSE).
- CNFRefutation (CRf): A refutation in clause normal form, including, for FOF Ax or C, the translation from FOF to CNF (without the FOF to CNF translation it is an IncompleteRefutation).
- Interpretation (Int): An interpretation.
- DomainInterpretation (DIn): An interpretation expressed as a domain, a mapping for functions, and a relation for predicates.
- FiniteInterpretation (FIn): A domain interpretation with a finite domain.
- InfiniteInterpretation (IIn): A domain interpretation with an infinite domain.
- HerbrandInterpretation (HIn): A Herbrand interpretation.
- Model (Mod): A model.
- DomainModel (DMo): A model expressed as a domain, a mapping for functions, and a relation for predicates.
- FiniteModel (FMo): A domain model with a finite domain.
- InfiniteModel (IMo): A domain model with an infinite domain.
- HerbrandModel (HMo): A Herbrand model.
- Saturation (Sat): A model expressed as a saturating set of formulae.
- ListofFormulae (Lof): A list of formulae.
- ListofTHF (Lth): A list of THF formulae.
- ListofFOF (Lfo): A list of FOF formulae.
- ListofCNF (Lcn): A list of CNF formulae.
- IncompleteProof (IPr): A proof with part missing.
- IncompleteRefutation (IRf): A refutation with parts missing.
- IncompleteCNFRefutation (ICf): A CNF refutation with parts missing.
- Assurance (Ass): Only an assurance of the success ontology value.
- None (Non): Nothing.
