Axiom names

From Ontohub
Revision as of 20:06, 4 May 2017 by Tillmo (talk | contribs) (started page)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

It is useful to label axioms and conjectures with self-explanatory names. This pays off especially when using a theorem prover with Hets or Ontohub, because then these names can be used to quickly select both axioms and conjectures (proof goals).

DOL

In DOL, axiom labels are written as follows:

. axiom %(axiom_label)%

OWL

In OWL Manchester syntax, axioms can be labeled using an rdfs:label annotation:

 Class: Woman SubClassOf: Annotations: rdfs:label "WomanSubClassOfPerson" Person

see also some example file