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).


In DOL, axiom labels are written as follows:

. axiom %(axiom_label)%


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