Contributors:
...
The IOF AnnotationVocabulary (AV) OWL file (AnnotationVocabulary) is the normative source for IOF annotation properties. It includes a superset of the annotation properties discussed in this document along with the metadata about them. This document’s purpose is to provide the requirements and instructions for authors of IOF ontologies. The AV should be imported into IOF ontologies under development to make these annotation properties available; however, since the IOF Core imports IOF AV, using AV requires no explicit owl:imports
statement.
The rules in this document changed some of the annotations needed by IOF ontologies as compared to those used in Core beta and before, deprecating at least one annotation property and adding a few additional. A revision of the AV consistent with this document was uploaded to the iofoundry/CoreDev GitHub repo (only) 2 Aug 2022, but older versions of the AV will not provide complete support.
All approved ontologies MUST adhere to the following annotation requirements for all constructs.
...
natural language definition –
iof-av:naturalLanguageDefinition
Definition: plain text for industry practitioner understanding
The natural language definition MUST be given for all constructs
Note: this definition MUST be present for both primitive constructs and non-primitive
The natural language definition MUST occur exactly once
The definition MUST adhere to ISO 704 rules and requirements for terminology
For non-primitive constructs, the natural language definition MUST NOT be circular
For primitive constructs, the natural language definition SHOULD NOT be circular
The definition MUST be substitutable in a sentence where the term appears
We MAY reconsider this as a requirement if there is no way to express it as a formal substitutable definition. There MUST be a rationale, expressed as an
explanatory note
, for why this is the case and the rationale MUST be agreed to by the Architecture TG.
The definition MUST NOT begin with an article (The, A or An).
One SHOULD avoid jargon and domain-specific terminology
It MUST be understandable by a practitioner in the industrial domain
It MUST NOT use specialized ontological terminology
Examples: perdurant, endurant, continuant, etc.
Ontological construct label MUST be provided in parenthesis
Example: role held by (bearer of) a material entity when it is a proper part of another material entity or is planned to be a proper part of another material entity
It MUST NOT use special formatting for properties or classes referenced in the definition
MUST NOT use upper camel case capitalization
MUST NOT use apostrophes to contain terms as a parenthetical
Examples: must not be as follows: ‘part-of’, ‘Information Content Entity', InformationContentEntity
It MUST NOT contain acronyms or abbreviations
Acronyms MAY be accepted if they appear in the dictionary and are widely used in conversation. Acronym use MUST be approved by the Architecture TG.
If the definition is taken from another source,
dcterms:source
or one of its sub-properties MUST cite the original reference. Seedcterms:source
in the Source Annotations section below.Examples:
shipment preparation process: planned process in which some material entities are prepared to be transported together to a receiver’s location
postal address: designation of a location (site) to which mail is delivered
Primitive Term Annotations
elucidation-- iof-av:elucidationelucidation MUST NOT be used and is deprecated.
is primitive –
iof-av:isPrimitive
Definition: boolean flag indicating that necessary and sufficient conditions are not provided
is primitive MUST be present if the term does not have necessary and sufficient conditions and the value of the annotation MUST be set to
true
(w3c boolean)Otherwise, if necessary and sufficient conditions are present, then the annotation MAY be provided and the value MUST be set to
false
is primitiveMUST default to set to
false
If possible, terms SHOULD have necessary and sufficient conditions
Note: the term may not always remain primitive if necessary and sufficient conditions can be defined in a later version
Example:
person: true
shipment preparation process: true
primitive rationale –
iof-av:primitiveRationale
Definition: reason why the necessary and sufficient conditions could not be provided
When is primitive is set to
true
, the primitive rationale MUST be providedThe primitive rationale MUST explain why necessary and sufficient conditions are not possible
The rationale SHOULD indicate what is missing if additional work is required to define necessary and sufficient conditions
Example:
person: insufficient constructs to create necessary and sufficient conditions
shipment preparation process: shipment preparation process often includes at least one picking, internal movement, packaging, marking, weighing, or loading process, but since those processes are not added to the ontology yet, it is not possible to generate necessary and sufficient conditions at this time for this entity
...
Symbol | Meaning | UTF-8 Code |
---|---|---|
∧ | Conjunction | U+2227 |
∨ | Disjunction | U+2228 |
¬ | Negation | U+00AC |
∃ | Existential Quantification | U+2203 |
∀ | Universal Quantification | U+27C7 |
→ | Implication/Conditional | U+2192 |
↔ | Equivalence/Bi-Implication | U+2194 |
( ) | Left/Right Parentheses | Left: U+0028, Right: U+0029 |
[ ] | Left/Right Square Brackets | Left: U+005B, Right: U+005D |
{ } | Left/Right Braces | Left: U+007B, Right: U+007D |
Examples:
product
:obo:Continuant(c) ∧ ¬(obo:SpecificallyDependentContinuant(c) ∨ Person(c) ∨ Organization(c)) ∧ ∃r (ProductRole(r) ∧ obo:hasRole(c, r))
semi-formal natural language definition –
iof-av:semiFormalNaturalLanguageDefinition
Definition: transitional definition expressing first-order logic definition using semantics understandable by ontologically knowledgable domain practitioner without predicate logic semantics
The semi-formal natural language definition MUST be provided if the term is not primitive (is primitive is
false
)The semi-formal natural language definition MUST only occur once
Variables SHOULD be removed if they do not need to be referenced later in the expression
Rules for writing necessary axioms, sufficient axioms, and necessary and sufficient axioms:
SHOULD use “every instance of {term} is defined as exactly an instance of {conditions}” for necessary and sufficient conditions
Example (Necessary and Sufficient Axiom): ‘agent’:
Agent(x) ↔ (Person(x) ∨ GroupOfAgents(x) ∨ EngineeredSystem(x)) ∧ ∃y (AgentRole(y) ∧ hasRole(x,y))
every instance of ‘agent’ is defined as exactly an instance of ‘person’, ‘group of agents’, or ‘engineered system’ that ‘has role’ some ‘agent role’
The following syntax MUST be used:
A construct label MUST be used and its exact syntax preserved for constructs in this or an imported ontology
Quotes (
'
) MUST surround all labelsThe words “is a” MUST NOT be used without a qualification
“is a subclass of” MUST be used to indicate a subclass relationship
“is an instance of” MUST be used to indicate an instance of a universal
Variables SHOULD be used where needed in formulating the definition
The rules for natural language definitions MUST be applied otherwise
Examples:
‘product’: every instance of ‘product' is defined as exactly an instance of (‘continuant’ and not ‘person’ and not ‘organization’ and not ‘specifically dependent continuant’) that ‘bears' some ‘product role’
‘agent’: every instance of ‘agent’ is defined as exactly an instance of ‘person’, ‘group of agents’, or ‘engineered system’ that ‘has role’ some ‘agent role’
logic axiom -
iof-av:logicAxiom
Definition: logical statements constraining the interpretation of the notion represented by the construct that does not provide necessary and sufficient conditions
Note: This annotation property is an abstraction of the more specialized logic axiom annotations used in IOF. However, this annotation property can also be used to group the logic axiom annotation values of different forms (such as FOL and natural language) that express the same meaning for a particular construct
A first-order logic axiom expression and a semi-formal natural language axiom expression SHOULD be added as property values for each logic axiom annotation using one of each of the corresponding logic axiom annotation sub-properties
Example:
Code Block iof-av:logicAxiom [ iof-av:firstOrderLogicAxiom "GenericallyDependentContinuant(x) ∧ ∃e(Entity(e) ∧ isAbout(x,e)) ->InformationContentEntity(x)" ; iof-av:semiFormalNaturalLanguageAxiom "x is a 'Generically Dependent Continuant' that 'is About' some 'Entity' e implies x is an 'Information Content Entity'" ; ] .
first-order logic axiom -
iof-av:firstOrderLogicAxiom
Definition: axiom of construct using predicate logic semantics
First-order logic axiom MAY be provided if the construct is primitive or non-primitive.
With the implication arrow → the left is sufficient and the right is necessary
A construct MAY have more than one first-order logic axiom annotation
A first-order logic axiom value MUST adhere to first-order logic definition syntax
If there is more than one axiom, the axiom MUST be associated with the semi-formal natural axiom
Examples:
GenericallyDependentContinuant(x) ∧ ∃e(Entity(e) ∧ isAbout(x,e)) →
InformationContentEntity(x)
semi-formal natural language axiom -
iof-av:semiFormalNaturalLanguageAxiom
Definition: transitional definition expressing first-order logic axiom using semantics understandable by ontologically knowledgable domain practitioner without predicate logic semantics
Semi-formal natural language axioms MAY be provided if the term is primitive (is primitive is
true
)A construct MAY include more than one semi-formal natural language axiom annotation
The definition MUST adhere to semi-formal natural language definition syntax
If there is more than one axiom, the axiom MUST be associated with the first-order logic axiom
All variables refer to instances
Rules for writing a necessary or sufficient axiom:
SHOULD use if and then to indicate the implication/conditional pattern for necessary or sufficient axiom: if antecedent, then consequent
AgentRole(x) → Role(x) ∧ ∃m ∃n ((MaterialEntity(m) ∧ ¬FiatObjectPart(x)) ∧ (Person(n) ∨ GroupOfAgents(n) ∨ EngineeredSystem(n)) ∧ actsOnBehalfOfAtSomeTime(m, n) ∧ roleOf(x,m))
'agent role': if x is an instance of 'agent role', then x is an instance of 'role' that is the 'role of' some ('material entity' and not 'fiat object part') that 'acts on behalf of at some time' some other 'person', 'group of agents', or 'engineered system'
SHOULD use some type of for a universal pattern
InformationContentEntity(x) ∧ ∃c, ∃r ( continuant(c) ∧ RequirementSpecification(r) ∧ satisfies(x,r) ∧ prescribes(x,c)) ∧ ∀c'(prescribes(x,c') → Continuant(c')) → DesignSpecification(x)
if d is a ‘design specification’, then d is an ‘information content entity’ that ‘prescribes' some type of 'continuant'
SHOULD use whenever when representing a multi-place temporal expression
∀ p,q,t (hasContinuantPart(p, q, t) ∧ instanceOf(p, MaterialEntity, t) → instanceOf(q, site, t) ∨ instanceOf(q, ContinuantFiatBoundary, t) ∨ instanceOf(q, MaterialEntity, t)
whenever a ‘material entity’ ‘has part’ y then y must be a ‘site’ or a ‘material entity’ or a ‘continuant fiat boundary’
...
direct source –
iof-av:directSource
Definition: definitive source of the subject resource
adapted from –
iof-av:adaptedFrom
Definition: source for the resource that was modified to create the subject resource
...
comment–rdfs:commentcomment MUST NOT be used. Use one of the following instead:
iof-av:explanatoryNote
iof-av:usageNote
skos:scopeNote
explanatory note –
iof-av:explanatoryNote
Definition: supplemental information used to clarify or describe the construct
explanatory note MAY be used to supplement the natural language definition of the construct
Example: “Item is another term semantically close to Product. But it is more general because Item may not sellable. It is an overloaded term used by information systems to capture catalog information about real and sort of unreal (e.g., product family or option class which is a group of similar products) materials the enterprise concerns with.”
usage note –
iof-av:usageNote
Definition: describes how to use the term in particular situations
usage note MAY be used to describe how the term is used in particular situations through an example instantiation.
Example: “This is how the Supplying Relation class may be used to convey who supplies what to who. SupplierRole(sr1) and BuyerRole(br1) and Product(p1) and SupplyingRelation(s1) and specificallyDependsOn(s1, sr1) and specificallyDependsOn(br1, s1) and specificallyDependsOn(p1,s1)”
scope note –
skos:scopeNote
If required, scope note MUST be used to provide additional domain contextualization on the use of the term
From skos:
A note that helps to clarify the meaning and/or the use of a concept
Example:
...
General Rules
Synonyms and abbreviations MUST include language tag
xml:lang
.
synonym –
iof-av:synonym
Definition: alternate label that may help users discover the construct
synonym MAY be used to indicate alternate term. If alternate term is context specific, it SHOULD be supplemented with the scope note annotation.
Example:
“process plan” is a synonym for the “plan specification” in the context/scope of discrete manufacturing, “recipe” is a synonym for the “plan specification” in the context/scope of batch and continuous manufacturing.
symbol –
iof-av:symbol
Definition: terse designation (abbreviation) for the construct
One SHOULD use symbol when a commonly used abbreviation exists, such as chemical symbols or units of measure
Examples:
m (meter)
C (carbon)
abbreviation –
iof-av:abbreviation
Definition: alternate short label for the element
OneSHOULDuse abbreviation when there is an alternate short label
One MUST use symbol if the abbreviation is a chemical or unit of measure.
acronym –
iof-av:acronym
Definition: specialized abbreviation
One SHOULD use acronym when there is a commonly accepted acronym
Examples:
PLM (Product Lifecycle Maintenance)
CAD (Computer Aided Design)
...
copyright –
iof-av:copyright
Definition: originator’s and authorized entity’s exclusive legal right to print, distribute, and publish material
Inspired by OED.
Ontologies MUST have a copyright annotation
license –
dcterms:license
Defintion: legal document giving official permission to do something with the resource [dcterms]
Ontologies MUST have a license annotation
abstract -
dcterms:abstract
Definition: A summary of the resource [dcterms]
Ontologies MUST have an abstract annotation
...
ISO 704
ISO 10241
ISO/IEC 21383-2:2020 (EN) Information Technology – Top-Level Ontology – Basic Formal Ontology
Link w/o paywall?
6.2.3.2 Upper case characters, mathematical symbols, typographical signs and syntactic signs (e.g. punctuation marks, hyphens, parentheses, square brackets and other connectors or delimiters) as well as their character styles (i.e. fonts and bold, italic, bold italic, or other style conventions) shall be used in a term only if they constitute part of the normal written form of the term as conventionally used in running text. Syntactic signs shall not be used to show alternative terms. For complex terms (e.g. compounds and multiword terms), the natural word order shall be retained.
...
Examples and discussion
for necessary and sufficient conditions
Example (Necessary Axiom): if d is an instance of ‘design specification’, then d is an instance of ‘information content entity’ that ‘prescribes' only instances of 'continuant' (if any)
Alt 2: if d is an instance of ‘design specification’, then d is an instance of ‘information content entity’ that ‘prescribes' only instances of 'continuant'
Alt 3: if d is a ‘design specification’, then d is an ‘information content entity’ that ‘prescribes' some 'continuant'
** BS Alt 4: if d is a ‘design specification’, then d is an ‘information content entity’ that ‘prescribes' some type of 'continuant'
SK Alt 5: if d is a ‘design specification’, then d is an instance of ‘information content entity’ that ‘prescribes’ some type of ‘entity’, and if so, the entity must be a ‘continuant’
Alt 6: if d is a ‘design specification’, then d is an ‘information content entity’ that ‘prescribes' only types of 'continuant'
Example (Sufficient Axiom): if x is an ‘information content entity’ that ‘prescribes' some (‘process characteristic’ or ‘capability’ or 'continuant') that is the 'output of' some 'process', thenx is an 'objective specification’
Domain and Range:
domain(R,C) iff for all x,y (xRy --> Cx)
range(R,C') iff for all x,y (xRy --> C'y)
We need an example for: (maybe one from BFO)
Foo ⊑ ∀ foobar.Bar
Without proofreading:
∀ x (Foo(x) → (∃ y(foobar(x,y) → Bar(y))))JL thinks the FOL would be this: ∀x,y(Foo(x) → (∀y(foobar(x,y) → Bar(y)))
JL first proposed text: “If x is an instance of ‘foo’, then if x has a ‘foobar’ relationship with y, then y is an instance of Bar“
Examples:
if x is a 'generically dependent continuant' that 'is about' some 'entity' then x is an 'information content entity'
‘algorithm’: if x is an instance of ‘plan specification’ that ‘prescribes' some ‘computing process’, then x is an 'algorithm’
x is an Algorithm if and only if x is a PlanSpecification and there is some y such that y is a ComputingProcess and y prescribes x
Which is equivalent of the conjunction of the following two assertions
if x is a PlanSpecification and there is some y such that y is a ComputingProcess and y prescribes x, then x is an Algorithm
if x is an Algorithm, then x is a PlanSpecification and there is some y such that y is a ComputingProcess and y prescribes x
'agent role': if x is an instance of 'agent role', then x is an instance of 'role' that is the 'role of' some ('material entity' and not 'fiat object part') that 'acts on behalf of at some time' some other 'person', 'group of agents', or 'engineered system'
Milos:
∀x,y(Foo(x) ∧ foobar(x,y) → Bar(y)))
∀x (Foo(x) → (∀y(foobar(x,y) → Bar(y)))
∀x (Foo(x) → (∀y(¬(foobar(x,y)) ∨Bar(y)))
Milos BFO Examples:
From BFO:
If a ‘has continuant part’ b then if a is an instance of ‘material entity’ then b is an instance of ‘site’ or ‘continuant fiat boundary’ or
'material entity' [mic-1]Corresponding owl axiom:
'has continuant part at some time' only (site or 'material entity' or 'continuant fiat boundary')
Proposed IOF axiom:
if x ‘has continuant part at some time’ y then y must be an instance of ‘site’ or ‘material entity’ or ‘continuant fiat boundary’
From BFO: b has continuant part c at some time =Def for some time t (b and c are continuants & b is a part of c at t)
Alternatively:
There exists no y for which x ‘has continuant part at some time’ y holds that is not an instance of ‘site’ or ‘material entity’ or ‘continuant fiat boundary’
FOL: ∀ p,q,t (hasContinuantPart(p, q, t) ∧ instanceOf(p, MaterialEntity, t) → instanceOf(q, site, t) ∨ instanceOf(q, ContinuantFiatBoundary, t) ∨ instanceOf(q, MaterialEntity, t)
To be translated to CL eventually.
With the temporal relation: (solution for multi-place temporal relation). Use whenever for t. x ‘has continuant part at some time’ y → whenever x ‘has part’ y
'at some time' → wheneverA. whenever a ‘material entity’ ‘has continuant part’ y then y must be a ‘site’ or a ‘material entity’ or a ‘continuant fiat boundary’
** B. whenever a ‘material entity’ ‘has part’ y then y must be a ‘site’ or a ‘material entity’ or a ‘continuant fiat boundary’
Rationale: we need to write the FOL for the future, but not introduce new predicates
C. whenever a ‘material entity’ ‘has part’ y then y must be a ‘site’ or a ‘material entity’ or a ‘continuant fiat boundary’ (and every part of a ‘material entity’ is a ‘continuant’)
D. whenever a ‘material entity’ ‘has part’ y then y must be a ‘site’ or a ‘material entity’ or a ‘continuant fiat boundary’
every part of a ‘material entity’ is a ‘continuant’
...