Version History

...

Contents

...

1. MUST: This word means that the definition is an absolute requirement of the specification.

2. MUST NOT: This phrase means that the definition is an absolute prohibition of the specification.

3. SHOULD: This word means that there may exist valid reasons in particular circumstances to ignore a particular item, but the full implications MUST be understood and carefully weighed before choosing a different course.

4. SHOULD NOT: This phrase means that there may exist valid reasons in particular circumstances when the particular behavior is acceptable or even useful, but the full implications should be understood and the case carefully weighed before implementing any behavior described with this label.

5. MAY: This word means that an item is truly optional. One user may choose to include the item because a particular marketplace requires it or because the vendor feels that it enhances the product, while another vendor may omit the same item.

...

• 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

      • 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 labels

    • The 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’

...

• ISO 704

  • https://oagiscore.atlassian.net/wiki/pages/viewpageattachments.action?pageId=4399431681&preview=%2F4399431681%2F4399267856%2FISO704_2009.pdf

• ISO 10241

  • https://oagiscore.atlassian.net/wiki/download/attachments/3664838679/ISO_IEC_21838-1.pdf?api=v2

• 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' → whenever

      • A. 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’

...