ISO IEC 21838-1 pdf – Information technology — Top-level ontologies (TLO) — Part 1: Requirements
a) they are non-circular;b) they form a consistent set;c)they are concise.
NOTE 2 Concise signifies that the definition contains no redundant elements (for example, lists of examples,explanations of usage, and so on).
These requirements apply both to the natural language definitions and also to the definitions providedin the oWL 2 and CL axiomatizations referenced in 4.2-and 4.3.
Non-circularity excludes not only immediate circularity (where the defined term or a term withequivalent meaning is used in the definition) but also mediated circularity (for example, where a term isused in the definition of a second term, which is itself used in the definition of the first term).To ensurenon-circularity it is recommended that definitions are formulated as statements of singly necessaryand jointly sufficient conditions for the correct application of the defined term.
EXAMPLE Triangle = def. closed figure that lies in a plane and consists of exactly three straight lines.
Consistency of the collection of natural language definitions is shown through the development of anaxiomatization that is proven consistent, as described in 4.2 and 4.3.
NOTE 3 Consistency, non-circularity and conciseness of definitions are features that distinguish ontologiesfrom traditional dictionaries and other lexical resources.
4.1.2 Relations between textual artefact and axiomatizations of the TLO
The terms and relational expressions in the textual artefact shall be converted into symbols in theaxiomatizations. These symbols together form the signature of the resultant logical theory. They mayincorporate textual strings.
EXAMPLE The text string ‘is a’ is converted into the symbol ‘is_a’.
Terms and relational expressions in the textual artefact should have counterparts in the oWL 2axiomatization wherever this is feasible, given the expressivity of OWL.
Each definition in the textual artefact whose content is expressible in OWL 2 shall correspond in the0WL 2 axiomatization to a group of one or more axioms with a corresponding logical content.
All terms in the textual artefact shall correspond to terms in the CL axiomatization.
All definitions of non-primitive terms in the textual artefact shall correspond to axioms in the CLformalization.
4.2 Axiomatization in the Web Ontology Language (OWL 2 with direct semantics)4.2.1General
The TLO shall be made available via at least one machine-readable axiomatization in OWL 2 withthe direct semantics or in some description logic that is designated by w3C as a successor of OWL 2.The signature of the oWL axiomatization shall be identical, modulo the conversion from strings intosymbols and modulo the conversion of ternary into binary relational expressions, to the set of naturallanguage terms and relational expressions of the TLO as specified under 4.1. The axioms shouldrepresent the content of the natural language definitions described in 4.1 to the extent that this ispossible given the expressivity of owL 2.The axiomatization shall satisfy the conformity criteria inw3C Recommendation —owL 2 Web Ontology Language Direct Semantics.T’he axiomatization shall be proven consistent using standard 0WL reasoners. The axiomatization shall be interpretable in the CLaxiomatization described in 4.3.
In the 0WL2 axiomatization, terms and relational expressions are replaced by IRIs! used in accordancewith the rules in the w3C Recommendation — owL Web Ontology Language GuideP2l.
4.2.2Alternative owL2 Axiomatization
In some cases, in order to compensate for the restrictions on axiom closure in an 0WL 2 ontology,a TLOmay be provided with two or more 0WL 2 axiomatizations, neither of which is logically interpretablein the other (W3C Recommendation — oWL 2 Web Ontology Language Structural Specification andFunctional-Styie Syntax).Each such axiomatization shall however be logically interpretable in the CLaxiomatization and a specification shall be provided of how such 0WL 2 axiomatizations relate to eachother and why each is needed.
NOTE 1 In the simplest case, the axiomatizations form a set linearly ordered in terms of theory strength, wheretheory A is stronger than theory B when B is logically interpretable in A, but A is not logically interpretable in B.Theory B is logically interpretable in theory A if, and only if,the language of B can be translated into the languageof A so that every theorem of B is derivable in A.An ontology developed in 0WL 2 is always logically interpretablein CL, but not vice versa.
NOTE 2To define ‘axiom closure’, the import closure l(0) of an ontology 0 is first defined as the setcontaining 0 and all the ontologies that 0 imports. The axiom closure of 0 is then the smallest set that containsall the axioms in l[(0) when the anonymous individuals from different ontologies in l(0) are treated as beingdifferent (W3C Recommendation — oWL 2 Web Ontology Language Structural Specification and Functional-StyieSyntax).
4.3Axiomatization in a CL-conforming language
The TLO shall be made available via an axiomatization in a language conforming to ISO/IEC 24707.NOTE CL, a logical framework standardized for the purpose of facilitating exchange and transmission ofknowledge in computer-based systems, is the standard ontology development language defined in ISO/IEC24707.Many of the principles underlying a TLO – for example, regarding change, mereology, and temporal and spatiallocation – cannot be adequately expressed using 0WL but require the expressivity of first-order logic providedby CL. CL. is a family of formal languages with a common descriptive semantics. Since CL circumvents differencesin formal language syntax by focusing on a shared semantics, translations between distinct formal languages areeasier to automate.
EXAMPLES Languages conforming to CL specified in ISO/IEC 24707 are the Common Logic InterchangeFormat (CLIF), the Conceptual Graph Interchange Format (CGIF), and the XML-based notation for Common Logic(XCL).For details of how languages traditionally used in first-order logic (FoL) can also conform to ISO/IEC 24707,see Reference[7].
The signature of the CL axiomatization shall be identical, modulo the conversion from strings intosymbols, to the set of natural language terms and relational expressions of the ontology as specified in4.1.The axiomatization shall extend the oWL 2 DL axiomatization described in 4.3-in the sense that itsmodels shall also satisfy the CL translation of the 0WL 2 axiomatization. The axiomatization shall beproven consistent using standard automated theorem provers. The axiomatization shall be explicitlymodularized.