Dataform Ontology Meanings

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.