DataForm

The DataForm Ontology

The data ontology provides suitable values for describing the form of logical data. The ontology values are commonly used to describe data provided to justify a success ontology value, e.g., if an ATP system reports the success ontology value Theorem it might output a Proof to justify that.

• Data (Dat):
  Data output.

• LogicalData (LDa):
  Logical data.

• Solution (Sln):
  A solution.

• Proof (Prf):
  A proof.

• Interpretation (Int):
  An interpretation.

• ListOfFormulae (Lof):
  A list of formulae.

• Derivation (Der):
  A derivation (inference steps, possibly ending in the theorem).

• Refutation (Ref):
  A refutation (starting with Ax U ~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's an IncompleteProof).

• Interpretation (Int)

An interoretation.

• Model (Mod):
  A model.

• DomainInterpretation (DIn):
  An interpretation whose domain is not the Herbrand universe.

• FiniteInterpretation (FIn):
  A domain interpretation with a finite domain.

• InfiniteInterpretation (IIn):
  A domain interpretation with an infinite domain.

• DomainModel (DMo):
  A model whose domain is not the Herbrand universe.

• FiniteModel (FMo):
  A domain model with a finite domain.

• InfiniteModel (IMo):
  A domain model with an infinite domain.

• HerbrandInterpretation (HIn):
  A Herbrand interpretation.

• HerbrandModel (HMo):
  A Herbrand model.

• FormulaHerbrandInterpretation (FHi):
  A Herbrand interpretation defined by a set of formulae.

• FormulaHerbrandModel (FHm):
  A Herbrand model defined by a set of formulae.

• SaturationHerbrandInterpretation (SHi):
  A Herbrand interpretation expressed as a saturated set of formulae. Not sure if this ever exists.

• SaturationHerbrandModel (Sat):
  A Herbrand model expressed as a saturated set of formulae.

• NotASolution (NSo):
  Something that is not a well formed solution.

• Assurance (Ass):
  Only an assurance of the success ontology value.

• IncompleteProof (IPr):
  A proof with some part missing.

• IncompleteInterpretation (InI):
  An interpretation with some part missing.

• NonLogicalData (NLd):
  Non-logical output.

• Comment (Com):
  TPTP format comments (starting with %).

• FreeText (FTx):
  Anything you want.

• Verification (Ver):
  Free format output from a solution verifier.

• None (Non):
  Nothing.