]>
Distributed Ontology, Model, and Specification Language (DOL) Terminology Ontology
Copyright (c) 2015-2017 Object Management Group, Inc.
Copyright (c) 2014-2017 Thematix Partners LLC
Copyright (c) 2014-2017 Fraunhofer Fokus
Copyright (c) 2014-2017 MITRE
Copyright (c) 2014-2017 Otto-von-Guericke University of Magdeburg
Copyright (c) 2014-2017 Athan Services
DOL-terms.rdf
dol
This ontology covers the terminology of the Distributed Ontology, Model, and Specification Language (DOL) and is an informative part of its specification.
When using this ontology for implementation purposes including complete DOL FOL or rules support, see annotations marked as 'beyond OWL'. They can be modeled in FOL or using rules.
http://www.omg.org/spec/ODM/
http://www.w3.org/standards/techs/owl#w3c_all
is strictly stronger than
supports symbol kind
Intended domain - OMSLanguage, intended range - owl:Class that rdfs:subClassOf value NonLogicalSymbol
supports symbol kind
Intended inverse - supportsSymbolKind
conservatively extends to
object is a conservative extension of the subject
definitionally extends to
object is a definitional extension of the subject
entails
relation of logical entailment, expressing that all realizations of the subject are also realizations of the object
extends to
subject is a mapping of an extension, the object is the target of the extension mapping, i.e. the extended OMS
formalizes
subject is a precise mathematical entity capturing the object (which is an informal or semi-formal entity)
has alignment
subject is a DOL library, in which the object is an alignment between two participating OMS
has exact logical expressivity
subject language has exactly the expressivity of the object logic
has heterogeneous environment
relationship between the subject and a heterogeneous environment in which it is embedded or is associated with
has interpretation
subject is a DOL library, in which the object is an interpretation between two participating OMS
has language aspect
relation between an OMS language and its language aspects
has logic
The reasoners in Protege don't like us to say the following, which makes hasLogic a non-simple property. hasLogic is not used in cardinality restrictions, so it _should_ be OK to say the following, but in practice it doesn't work.
SubPropertyChain: semanticallyDenotes o hasLogic
specification of valid reasoning that comprises signatures (user defined vocabularies), realizations (interpretations of these), sentences (constraints on realizations), and a satisfaction relation between realizations and sentences, i.e., the logic in which an OMS is formalized
has mapping
subject is a DOL library, in which the object is a mapping between two participating OMS
has member
inverse of the set membership relation
has realizations
OMS (resp. its semantic object) has an associated class of realizations (models), which is the class of realizations of the OMS
has OMS
subject is a DOL library, in which the object is a participating heterogeneous OMS
has part
relationship between two things were the second is a component of the first
has proficiency
property of a tool that is capable of implementing a process
has sentences
OMS (resp. its semantic object) has an associated set of sentences, that is the set of sentences of the OMS
has sequence member
inverse of the sequence membership relation
This is a lingustic property, because it is about sequences of linguistic entities that occur in a text.
has signature
OMS (resp. its semantic object) has an associated signature, which is the signature of the OMS
has source
source OMS of a mapping
has target
target OMS of a mapping
implied extends to
relation of a model-theoretic conservative extension that does not introduce new non-logical symbols
is adjoint of
subject is a translation (or reduction) that shares its sentence and realization translation with the object reduction (or translation)
The signature translations are adjoint to each other (in the sense of category theory).
is alignment in
object is a DOL library, in which the subject is an alignment between two participating OMS
is approximant of
approximation (in the sense of a logically implied theory, possibly aftersuitable translation) of an OMS in a smaller signature or OMS language
is combination of OMS
Consider an ontology involving a concept Person, and another one involving Human being, and an alignment that relates these to concepts. In the combination of the ontologies along the alignment, there is only one concept, representing both Person and Human being.
aggregation of all the OMS in an OMS network, where non-logical symbols are shared according to the OMS mappings in the OMS network
is composition of
subject mapping is the composition of the object list of mapping
Essentially, this means list item 1 composed with list item 2 composed with … composed with list item n. All elements of the latter list must be instances of the same class as the subject. (Note that enforcing the latter constraint goes beyond OWL, and the range cannot be specified in OWL DL.)
is consequence theoretically conservative extension of
subject OMS is a consequence-theoretic conservative extension of the object OMS
A consequence-theoretic conservative extension is an extension that does not add new theorems (in terms of the unextended signature).
is conservative extension of
subject is a conservative extension of the object
is definitional extension of
$O_2$ being a definitional extension of $O_1$ implies a bijective correspondence between the classes of realizations of $O_2$ and $O_1$.
An extension $O_2$ of an OMS $O_1$ is a definitional extension, if each realization of $O_1$ can be uniquely expanded to a realization of $O_2$.
Each definitional extension is also a monomorphic extension but not vice versa.
We need FOL, or the same reification approach as chosen for the different kinds of translations, for capturing that an extension is definitional if and only if it is weakly definitional and model-theoretically conservative.
extension whose newly introduced non-logical symbols are interpreted in a unique way
isMonomorphicExtensionOf
is element of OMS
any resource in an OMS (e.g. a non-logical symbol, a sentence, a correspondence, the OMS itself, ...) or a named set of such resources
is embeddable into
subject is embeddable into the object logic
is entailed by
inverse of relation of logical entailment
is exactly mappable to
an exact mapping from the subject to the object logic
relation between two OMS whereby the subject OMS is an extension of the object OMS, i.e. the sets of non-logical symbols and sentences of the subject OMS are supersets of those of the object OMS
extends
is extension of
is faithfully mappable to
a faithful mapping from the subject to the object logic
is formalized by
object is a precise mathematical entity capturing the subject (which is an informal or semi-formal entity)
is implied extension of
A conservative extension $O_2$ of an OMS $O_1$ is an implied extension, if and only if the signature of $O_2$ is the signature of $O_1$. $O_2$ is an implied extension of $O_1$ if and only if the realization class of $O_2$ is the realization class of $O_1$.
Each implied extension is also a definitional extension but not vice versa.
model-theoretic conservative extension that does not introduce new non-logical symbols
isConservativeExtensionOf
is interpretation in
object is a DOL library in which the subject is an interpretation between two participating OMS
is language aspect of
set of language constructs of a given language, not necessarily forming a sublanguage
is language of
The reasoners in Protege don't like us to say the following. Together with the SubPropertyChain specified for supportsSerialization it would go beyond OWL DL anyway.
SubPropertyChain: serialization o serializes
language of an OMS
is linguistically related to
relation between linguistic entities
is logically interoperable with
property of structured OMS, which may be written in different OMS languages supporting different logics, of being usable jointly in a coherent way (via suitable OMS language translations), such that the notions of their overall consistency and logical entailment have a precise logical semantics
is logically related to
relation between lingustic entities that has a logical, semantic nature
is mappable from
indicates that there is a mapping from the object to the subject
mappable from language
indicates that there is a mapping from the object language to the subject language
mappable from logic
indicates that there is a mapping from the object logic to the subject logic
is mappable to
indicates that there is a mapping from the subject to the object
is mappable to bijectively on models
indicates a realization-bijective mapping from the subject to the object logic
is mappable to language
indicates that there is a mapping from the subject language to the object language
is mappable to logic
indicates that there is a mapping from the subject logic to the object logic
is mapped by
object mapping maps from the subject into something of the same type as the subject
is mapping in
object is a DOL library, in which the subject is a mapping between two participating OMS
is mathematically related to
relation between mathematical entities
is member of
set membership relation
is model expansively mappable to
indicates that there is a realization-expansive mapping from the subject to the object logic
is a realization of the OMS
relationship between a realization and an OMS where the realization is a member of the realization class of the OMS (which for flattenable OMS is equivalent to being a realization of the signature of the OMS and satisfying all sentences in the OMS)
is a realization of the signature
relationship between a realization and a signature (vocabulary) such that the realization provides a semantic interpretation of all non-logical symbols in the signature
is model theoretically conservative extension of
the subject OMS is a model-theoretic conservative extension of the object OMS. A model-theoretic conservative extension is an extension that does not lead to a restriction of class of realizations (models) of an OMS
isConsequenceTheoreticallyConservativeExtensionOf
is module of
relationship between two OMS where the first conservatively extends to the second OMS
is monomorphic extension of
subject OMS is a monomorphic extension of the object OMS
A monomorphic extension is an extension whose newly introduced non-logical symbols are interpreted in a way unique up to isomorphism.
isModelTheoreticallyConservativeExtensionOf
is OMS documentation of
relationship between an OMS documentation and the documented OMS
is union of OMS
structured OMS expressing the combination of all constraints of a sequences of OMS
is OMS in
subject is an OMS participating in a DOL library, which is the object
is plainly mappable to
indicates that there is a plain mapping from the subject to the object logic
is profile of
subject is a profile of the object language
This is a stronger notion than just being a sublanguage. Supported serializations are shared along this property.
is reducible from
indicates that there is a reduction from the object to the subject
is reducible to
indicates that there is a reduction from the subject to the object
is related as part of maps to
property used in the context of mappings, for both linguistic and mathematical entities
is semantically related to
relation that has a semantic nature
is sequence memberOf
sequence membership relation
is serialized in
the textual syntax in which an OMS is written
is simply theoroidally mappable to
indicates that there is a simple theoroidal mapping from the subject to the object logic
is source of mapping
object mapping maps from the subject into something of the same type as the subject
is sublanguage of
syntactically specified subset of a given language, consisting of a subset of its terminal and nonterminal symbols and grammar rules
Supported logics are shared along the inverse of this property.
is sublogic of
logic that is a syntactic restriction of another logic, inheriting its semantics
is subOMS of
OMS whose sets of non-logical symbols and sentences are subsets of those present in a given larger OMS
is translatable from
indicates that there is a translation from the object to the subject
is translatable to
indicates that there is a translation from the subject to the object
is weak definitional extension of
subject OMS is a weak definitional extension of the object OMS
A weak definitional extension is an extension whose newly introduced non-logical symbols can be interpreted in at most one way.
is weakly exactly mappable to
indicates that there is a weakly exact mapping from the subject to the object logic
maps from
Enforcing the constraint that a mapping must map into something of the same type goes beyond OWL.
The subject mapping maps from the object into something of the same type as the object.
relationship between a mapping and its domain
maps to
The subject mapping maps from something into the object (which is of the same type). Enforcing the latter constraint goes beyond OWL.
relationship between a mapping and its codomain
is reified by
subject property is reified by the object class
reifies
subject class reifies the object property
Because of the punning issue in OWL DL, this property is used in restrictions that explicitly do not include the target object property. The target property is identified instead in a usage note on the class that reifies that property, which can be codified in a rule or FOL.
satisfies
relationship between a realization and a sentence indicating that the sentence holds true in the realization
semantically denotes
relation between a linguistic entity and its semantic denotation
serializes
subject is a serialization for the object language; for example, Manchester syntax serializes OWL
shares with
Sharing is always relative to a given OMS network that relates different OMS. That is, two given OMS symbols
can share with respect to one OMS network, and not share with respect to some other OMS network.
property of OMS symbols being mapped to the same symbol when computing a combination of an OMS network
specifies semantics of
indicates that the semantics of [a subset of] the object language can be specified in terms of the subject logic
supports logic
The semantics of [a subset of] the subject language can be specified in terms of the object logic.
logic represented by a satisfaction relation of the language
supports logic mapping
subject language mapping corresponds to the object logic mapping
supports serialization
The reasoners in Protege don't like us to say the following. Together with the SubPropertyChain specified for language it would go beyond OWL DL anyway.
SubPropertyChain: isProfileOf o supportsSerialization
Note that the serialization should be as specific as possible, i.e. one should not say that 'OWL can be serialized in XML' and 'Common Logic can be serialized in XML', but instead 'OWL can be serialized in OWL XML' and 'Common Logic can be serialized in XCL', taking into account that OWL XML and XCL are two different XML languages.
OMS in the subject language can be serialized in the object serialization
uses language
relation between something and a language used by one or more components of it
an alternative filename extension for a serialization
the media type (MIME type) of a serialization
the preferred filename extension for a serialization
propagates to adjoint
subject class denotes a kind of mapping that, if it holds for a translation, also holds for the adjoint reduction
abstract syntax
An abstract syntax can be specified as a MOF metamodel. Then abstract abstract syntax documents can be represented as XMI documents.
term language for representing documents in a machine-processable way
alignment
an OMS mapping expressing a collection of relations between entities of the two OMS
an alignment between two heterogeneous OMS in a DOL library
annotation expression
Formally, an annotation can be specified as a (subject, predicate, object) triple, as defined in the RDF 1.1 W3C Recommendations. In the case of an annotation on an OMS, the subject of an annotation is an element of an OMS. The predicate is an RDF property defined in an external OMS that describes the way in which the annotation object is related to the annotation subject. Given this representation approach, it is possible to interpret annotations under an RDF semantics. 'Without a logical semantics' under this definition means that annotations to an OMS are not considered sentences of that OMS.
additional information without a logical semantics that is attached to an element of an OMS
annotation expression language aspect
the (unique) language aspect of an OMS language that enables the expression of comments and annotations
answer substitution
substitution that, when applied to a given query, turns the latter into a logical consequence of a given OMS
approximant
logically implied theory (possibly after suitable translation) of an OMS in a smaller signature or a sublanguage
approximation
structured OMS that expresses a maximum approximant
axiom
sentence postulated to be valid (i.e., true in every realization)
infrastructure axiom
axiom that used in a simple theoroidal mapping
basic OMS
1
a basic OMS (in a single language, logic, and serialization)
unstructured native OMS that may be used as a building block for a larger OMS, denoting a logical theory
category
In DOL, objects of a category are usually signatures or OMS, and morphisms are signature morphisms, or OMS mappings. In principle, no assumption about the exact nature of objects and morphisms is made.
The morphisms determine which part of the structure of the objects is relevant, i.e. preserved by morphisms. Hence, objects can be seen as 'sets with structure', and morphisms as 'structure-preserving maps'. However note that not all categories can be obtained in this way.
a class of objects with suitable morphisms between them
class of realizations
a class of realizations (over some signature in some logic)
closure
DOL supports four different forms of closure: minimization and maximization as well as freeness and cofreeness.
Symbols from the local environment are assumed to have a fixed interpretation. Only the symbols newly declared in the closure are forced to have minimal or maximal interpretation.
structured OMS expressing a variant of the closed world assumption by restricting the realizations to those that are minimal or maximal (with respect to the local environment)
The closed world assumption is a default assumption about facts whose status in unknown.
cofreeness
In first-order-like logics, cofreeness means maximal interpretation of predicates and equality being observable equivalence. Cofreeness can be used for the specification of coinductive datatypes like infinite lists and streams.
special type of closure, restriction of realizations to those that are cofree (with respect to the local environment)
collection of expressions
collection whose members are expressions
combination
Consider an ontology involving a concept Person, and another one involving Human being, and an alignment that relates these to concepts. In the combination of the ontologies along the alignment, there is only one concept, representing both Person and Human being.
structured OMS expressing the aggregation of all the OMS in an OMS network, where non-logical symbols are shared according to the OMS mappings in the OMS network
consequence-theoretic conservative extension
An extension O_2 of an OMS O_1 is a consequence-theoretic conservative extension, if all properties formulated in the signature of O_1 hold for O_1 whenever they hold for O_2.
extension that does not add new theorems (in terms of the unextended signature)
consequence-theoretic conservative extension mapping
1
An extension O_2 of an OMS O_1 is a consequence-theoretic conservative extension, if all properties formulated in the signature of O_1 hold for O_1 whenever they hold for O_2.
mapping of a consequence-theoretic conservative extension
reifies property isConsequenceTheoreticallyConservativeExtensionOf
conservative extension
extension that does not add new logical properties with respect to the signature of the extended OMS
conservative extension mapping
1
If used without qualification, the consequence-theoretic version is meant.
extension mapping of a consequence-theoretic or model-theoretic conservative extension
reifies property isConservativeExtensionOf
consistent OMS
OMS that has a non-trivial set of logical consequences in the sense that not every sentence follows from the OMS
correspondence
A correspondence is given as a quadruple (e_1, R, e_2, c), where R denotes the type of relationship that is asserted to hold between the two non-logical symbols or terms, and 0<=c<=1 is a confidence value. R and c may be omitted: When R is omitted, it defaults to the equivalence relation, unless another defaultrelation has been explicitly specified; when c is omitted, it defaults to 1.
relationship between a non-logical symbol e_1 from an OMS O_1 and a non-logical symbol e_2 from an OMS O_2, or between a non-logical symbol e_1 from O_1 and a term t_2 formed from non-logical symbols from O_2
DOL document
document containing a DOL library
DOL entity
entity that is used in DOL texts
DOL library
Collection is used here in the sense of syntactic collection.
collection of named OMS and OMS networks, possibly written in different OMS languages, linked by named OMS mappings
DOL structured OMS
DOL structured OMS, typically, use basic OMS as building blocks for defining other structured OMS, OMS mappings or OMS networks.
syntactically valid DOL expression denoting an OMS that is built from smaller OMS as building blocks
default logic mapping
true
logic mapping that will be chosen by default if only the source and target logic are given
default language mapping
true
language mapping that will be chosen by default if only the source and target language are given
default mapping
true
mapping that will be chosen by default if only the source and target are given
definitional extension
An extension O_2 of an OMS O_1 is a definitional extension, if each realization (model) of O_1 can be uniquely expanded to a realization of O_2.
extension whose newly introduced non-logical symbols are interpreted in a unique way
definitional extension mapping
O_2 being a definitional extension of O_1 implies a bijective correspondence between the classes of realizations of O_2 and O_1.
An extension O_2 of an OMS O_1 is a definitional extension, if each realization of O_1 can be uniquely expanded to a realization of O_2.
Each definitional extension is also a monomorphic extension but not vice versa.
mapping of a definition extension
1
reifies property isDefinitionalExtensionOf
document
text that typically is the result of serializing an object using a given serialization
In other words, typical documentthat is a linguistic entity used in context of the DOL standard contain an OMS or DOL library.
elusive OMS
OMS that is not flattenable
embedding
logic mapping that embeds the source into the target logic, using components that are injections and (in the case of realization translations) isomorphism
1
reifies property isEmbeddableInto
entailment
Entailment expresses that each realization satisfying the first OMS also satisfies the second OMS (or the sentence, respectively).
Entailments can also be stated between networks, or networks and OMS.
logical consequence
a relation between two OMS (or an OMS and a sentence, or two OMS networks, or an OMS network and an OMS) expressing that the second item (the conclusion) is logically implied by the first one (the premise)
equivalence
Two OMS are equivalent if they have a common definitional extension. The OMS may be written in different OMS languages.
OMS mapping ensuring that two OMS share the same definable concepts
exact mapping
true
logic mapping that is compatible with certain DOL structuring constructs
1
reifies property isExactlyMappableTo
expression
1
a finite combination of symbols that are well-formed according to applicable rules (depending on the language)
extension
The new symbols and sentences are interpreted relative to the local envorinment, which is the signature of the 'given OMS'.
structured OMS extending a given OMS with new symbols and sentences
extension mapping
This definition differs from that in the Terms and Definition section of the DOL specification by focussing on the mapping rather than the codomain of the mapping.
mapping of an extension
faithful mapping
true
logic mapping that preserves and reflects logical consequence
1
reifies property isFaithfullyMappableTo
filtering
If a symbol is removed, all axioms containing that symbol are removed, too.
structured OMS expressing the verbatim removal of symbols or axioms from an OMS
flattenable OMS
More precisely, an OMS is flattenable if and only if it is either a basic OMS or it is an extension, union, translation, module extraction, approximation, filtering, or reference of named OMS involving only flattenable OMS.
OMS that can be seen, by purely syntactical means, to be logically equivalent to a basic OMS
flattening
process of transforming an OMS to an equivalent basic OMS
formal semantics
A formal semantics is a formalization of the meaning of a language.
assignment of mathematical meaning to a language by mapping abstract syntax to suitable semantic domains
freeness
In first-order logic (and similar logics), freeness means minimal interpretation of predicates and minimal equality among data values. Freeness can be used for the specification of inductive datatypes like numbers, lists, trees, bags etc. In order to specify, e.g., lists over some elements, the specification of the elements should be in the local environment.
special type of closure, restriction of realizations to those that are free (with respect to the local environment)
global environment
mapping from identifiers (IRIs) to values in semantics domains representing semantic information about a set of documents (the latter typically being distributed over the internet)
graph
network
set of objects (nodes) that are connected by links (edges)
heterogeneous environment
environment for the expression of homogeneous and heterogeneous OMS, comprising a logic graph, an OMS language graph and a supports relation
The support relations specify which language supports which logics and which serializations, and which language translation supports which logic translation or reduction. Moreover, each language has a default logic and a default serialization.
Although in principle, there can be many heterogeneous environments, for ensuring interoperability, there will be a global heterogeneous environment (maintained in some registry), with subenvironments for specific purposes.
heterogeneous OMS
OMS whose parts are supported by different logics
homogeneous OMS
OMS whose parts are supported by one logic
implied extension
A conservative extension O_2 of an OMS O_1 is an implied extension, if and only if the signature of O_2 is the signature of O_1. O_2 is an implied extension of O_1 if and only if the realization class of O_2 is the realization class of O_1.
model-theoretic conservative extension that does not introduce new non-logical symbols
implied extension mapping
A conservative extension O_2 of an OMS O_1 is an implied extension, if and only if the signature of O_2 is the signature of O_1. O_2 is an implied extension of O_1 if and only if the realization class of O_2 is the realization class of O_1.
Each implied extension is also a definitional extension but not vice versa.
mapping of an implied extension
1
reifies property isImpliedExtensionOf
import
An owl:import in OWL is an import.
Importing O_1 into O_2 turns O_2 into an extension of O_1.
Semantically, an import of O_2 into O_1 is equivalent to the verbatim inclusion of O_2 in place of the import declaration.
The import of a whole DOL library into another DOL library is also called import.
The purpose of O_2 importing O_1 is to make non-logical symbols and sentences of O_1 available in O_2.
reference to an OMS or DOL library behaving as if it were verbatim included
inconsistent OMS
OMS that has a trivial set of logical consequences in the sense that every sentence follows from the OMS
institution
metaframework mathematically formalizing the notion of a logic in terms of notions of signature, signature morphism, realization, sentence and satisfaction
interface signature
signature mediating between an OMS and a module of that OMS in the sense that it contains those non-logical symbols that the sentences of the module and the sentences of the OMS have in common
interpretation
OMS mapping that postulates a specialization relation between two OMS along a morphism between their signatures
refinement
view
formal language
Collection is used here in the sense of syntactic collection.
collection of expressions, following formal rules of well-formedness
language
a body of words, following a set of methods of combining them (called a grammar), understood by a community and used as a form of communication
construct
syntactic pattern that is part of a language
language aspect
set of language constructs of a given language, not necessarily forming a sublanguage
OMS language graph
graph with OMS languages as nodes and OMS language translations and OMS language reductions as edges, typically used in a heterogeneous environment
language mapping
1
1
mapping between languages
linguistic entity
entity that is of linguistic, syntactic nature
linked data
RDF, serialized as RDF/XML, is the most common format for publishing linked data. However, its usage is not mandatory.
Linked data principles, as interpreted herein, are as follows: (a) Use IRIs as names for things; (b) Use HTTP IRIs so that these things can be referred to and looked up (dereferenced) by people and user agents; i.e., the IRI is treated as a URL (uniform resource locator); (c) Provide useful machine-processable (plus optionally human-readable) information about the thing when its IRI is dereferenced, using standard formats; (d) Include links to other, related IRIs in the exposed data to improve discovery of other related information on the Web.
Using HTTP content negotiation, it is possible to serve representations in different formats from the same URL.
structured data that is published on the Web in a machine-processable way, according to principles explained in http://linkeddata.org/
local environment
signature built from all previously-declared symbols and axioms
monotonic logic
SROIQ(D) is the logic underlying OWL 2 DL.
Most OMS languages have an underlying logic.
See the annexes in the DOL specification for an explanation of the organization of the relation between OMS languages and their logics and serializations.
a (monotonic) logic that defines the semantics of an language
specification of monotonic valid reasoning that comprises signatures, sentences, realizations, and a satisfaction relation between realizations and sentences
logic
SROIQ(D) is the monotonic logic underlying OWL 2 DL.
Reiter's default logic is a logic that is not monotonic.
Most OMS languages have an underlying logic.
See the annexes in the DOL specification for an explanation of the organization of the relation between OMS languages and their logics and serializations.
a (possibly non-monotonic) logic that defines the semantics of an language
specification of (possibly non-monotonic) valid reasoning that comprises signatures, sentences, realizations, and a satisfaction relation between realizations and sentences
logic graph
In a logic graph, some of the logic translations and reductions can be marked to be default translations.
graph with logics as nodes and logic translations and logic reductions as edges, typically used in a heterogeneous environment
logic mapping
1
1
1
1
true
a mapping (translation or reduction) between two logics consisting of mappings for signatures, sentences and realizations
mapping between logics
logic reduction
mapping between logics forgetting parts of the logical structure, projection to a smaller logic, in contrast to translation
reduction of a source logic onto a (usually less expressive) target logic (mapping signatures, sentences and realizations) that simply forgets those parts of the logical structure not fitting the target logic
reduction
mapping forgetting parts of the source, projection to a smaller target, in contrast to translation
reduction of a source onto a (usually less expressive) target that simply forgets those parts of the source not fitting the target
OMS language reduction
mapping between OMS languages forgetting parts of the source, projection to a smaller language, in contrast to translation
reduction of a source language onto a (usually less expressive) target language that simply forgets those parts of the source language not fitting the target language
An OMS language reduction shall satisfy the property that the result of a reduction is a well-formed text in the target language.
logic translation
mapping between logics representing all structure, in contrast to reduction
translation of a source logic into a target logic (mapping signatures, sentences and realizations) that keeps or encodes the logical content of OMS
translation
mapping representing the source completely, in contrast to reduction
mapping of a source into a target that keeps or encodes the content of the source
logical language aspect
the (unique) language aspect of an OMS language that enables the expression of non-logical symbols and sentences in a logical language
logical theory
1
1
The sentences must use only those non-logical symbols that are present in the signature.
a signature together with a set of sentences (over that signature)
model
Not to be confused with the term 'model' in the sense of logic (model theory), which is termed 'realization' in this ontology.
representation of (the development of) a system (e.g., hardware, software, information system, or organization), or a domain related to a system, used in model-driven engineering (MDE)
mapping
1
1
a generic set-theoretic mapping or family of set-theoretic mappings (translation or reduction)
function
in some cases is a morphism, as in Category Theory.
relation between a set of inputs and a set of permissible outputs with the property that each input is related to exactly one output
1
reifies property isMappableTo
matcher
tool that implements matching
matching
algorithmic procedure that generates an alignment for two given OMS
mathematical entity
entity that is part of a mathematical theory
maximization
form of closure that restricts the realizations to those that are maximal (with respect to the local environment)
maximum approximant
Technically, a maximum approximant is a uniform interpolant
best possible (in the sense of a maximum set of logical consequences) approximant of an OMS in a smaller signature or a sublanguage
minimization
Also known as circumscription.
form of closure that restricts the realizations to those that are minimal (with respect to the local environment)
realization
semantic interpretation of all non-logical symbols of a signature
A realization of an OMS is a realization of the signature of the OMS that also satisfies all the additional constraints expressed by the OMS. In case of flattenable OMS, these constraints are expressed by the axioms of the OMS.
This term is called 'realization' and not 'model' in order not to be confused with model in the sense of modeling (i.e., the 'M' in OMS).
model bijective mapping
true
logic mapping that has a bijective mapping of realizations (models)
1
reifies property isMappableToBijectivelyOnModels
model expansive mapping
true
logic mapping that has a surjective realization (model) translation (ensuring faithfulness of the mapping)
1
reifies property isModelExpansivelyMappableTo
model finder
tool that implements realization (model) finding
model finding
process that finds realizations (models) of an OMS and thus proves it to be satisfiable
model-theoretic conservative extension
An extension O_2 of an OMS O_1 is a model-theoretic conservative extension, if all properties formulated in the signature of O_1 hold for O_1 whenever they hold for O_2.
extension that does not lead to a restriction of class of models of an OMS
model-theoretic conservative extension mapping
An extension O_2 of an OMS O_1 is a model-theoretic conservative extension, if all properties formulated in the signature of O_1 hold for O_1 whenever they hold for O_2.
Any model-theoretic conservative extension is also a consequence-theoretic one.
mapping of a model-theoretic conservative extension
1
reifies property isModelTheoreticallyConservativeExtensionOf
module
structured OMS expressing a subOMS that conservatively extends to conservative extension the whole OMS
module extraction
Cited and slightly adapted from Suarez, Figueroa et al: Ontology Glossary 2008
The goal of module extraction is 'decomposing an OMS into smaller, more manageable modules with appropriate dependencies' \cite{DBLP:series/lncs/5445}
activity of obtaining from an OMS concrete modules to be used for a particular purpose (e.g., to contain a particular sub-signature of the original OMS)
module extractor
tool that implements module extraction
monomorphic extension
An extension O_2 of an OMS O_1 is a monomorphic extension, if each realization (model) of O_1 can be expanded to a realization of O_2 that is unique up to isomorphism.
extension whose newly introduced non-logical symbols are interpreted in a way unique up to isomorphism
monomorphic extension mapping
An extension O_2 of an OMS O_1 is a monomorphic extension, if each realization (model) of O_1 can be expanded to a realization of O_2 that is unique up to isomorphism.
Each monomorphic extension is also a model-theoretic conservative extension but not vice versa.
mapping of a monomorphic extension
1
reifies property isMonomorphicExtensionOf
native document
document containing a native OMS
native OMS
sequence of expressions (like non-logical symbols, sentences and structuring elements) from a given OMS language
non-logical symbol
Non-logical symbols in Common Logic (ISO/IEC 24707:2007) comprise (a) names (denoting objects from the domain of discourse), and (b) sequence markers (denoting sequences of objects). This is opposed to logical symbols in Common Logic, e.g., logical connectives and quantifiers.
Non-logical symbols in OWL (W3C/TR REC-owl2-syntax), called 'entities' therein, comprise \begin{itemize} \item individuals (denoting objects from the domain of discourse), \item classes (denoting sets of objects; also called concepts), and \item properties (denoting binary relations over objects; also called roles). \end{itemize} This is opposed to logical symbols in OWL, e.g.\ those for intersection and union of classes.
OMS symbol
The notion of 'atomic sentence' used in logic is different, it usually may involve several non-logical symbols.
a non-logical symbol in an OMS
symbol that requires an interpretation through a realization
logical symbol
Logical symbols in Common Logic include propositional connectives and quantifiers.
Logical symbols in OWL include propositional connectives (e.g. the intersection operator on classes) and quantifiers (e.g. the existential restriction operator).
symbol whose interpretation is fixed by the logic
symbol
atomic expression or syntactic constituent of an OMS
OMS (ontology, specification or model)
An OMS can be written in different OMS language serializations.
An OMS has a single signature and realization class over that signature as its model-theoretic semantics.
An OMS is a collection of expressions (like non-logical symbols, sentences and structuring elements) in a given OMS language (or several such languages) and denoting a class of realizations and, possibly, a logical theory
a basic or structured ontology, specification or model
collection is used here in the sense of syntactic collection
OMS documentation
Adapted from SuarezFigueroaEtAl:OntologyGlossary2008
set of all annotations to an OMS, plus any other documents and explanatory comments generated during the entire OMS building process
OMS language
An OMS language is used for the formal specification of OMS.
OMS languages include OWL, Common Logic, F-logic, UML class diagrams, RDFS, and OBO.
a language for OMS (ontologies, models or specifications)
language equipped with a formal, declarative, logic-based semantics, plus non-logical annotations
OMS language translation
1
1
1
1
true
An OMS language translation shall satisfy the property that the result of a translation is well-formed in the target language.
a translation between two OMS languages that keeps or encodes the content of the source
OMS mapping
1
1
a mapping between two heterogeneous OMS in a DOL library
relationship between two OMS, typically given as a set of correspondences
1
reifies property isMappableTo
OMS network
An OMS network is a diagram of OMS in the sense of category theory, but different from a diagram in the sense of model-driven architecture.
collection is used here in the sense of syntactic collection
collection of named OMS, possibly written in different OMS languages, linked by named OMS mappings and named OMS networks
the definition deliberately includes OMS networks; this is a recursive definition. A specific network can make use of this recursion only finitely many times.
hyperontology
OMS reduction
DOL structured OMS expressing the restriction of an OMS to a smaller signature
1
reifies property isReducibleTo
OMS Semantic Object
object giving the semantics of an OMS
OMS translation
An OMS translation results in an OMS mapping between the original and the translation OMS.
DOL structured OMS expressing the assignment of new names to some non-logical symbols of an OMS, or translation of an OMS along a language translation
ontology
explicit and shared formal representation of the entities and their interrelationships of a given domain of discourse or of fundamental notions
The explicit and shared formal representation is materialised in some OMS language (or several such languages).
Ontologies also include definitions and explanations in natural language that capture the intended meaning of the formal expressions.
Ontologies typically include a taxonomy and, frequently, a partonomy.
plain mapping
true
Developers' note: Protégé 4.2 doesn't like 'Class: OMSMapping DisjointUnionOf: PlainMapping, SimpleTheoroidalMapping', so we do it this way:
logic mapping that maps signatures to signatures and therefore does not use infrastructure axioms
1
reifies property isPlainlyMappableTo
Developers' note: Protégé 4.2 doesn't like 'Class: OMSMapping DisjointUnionOf: PlainMapping, SimpleTheoroidalMapping', so we do it this way:
process
algorithmic procedure working on DOL-related linguistic entities as input
profile
Profiles can have different logics, even with completely different semantics, e.g., OWL 2 DL versus OWL 2 Full.
The logic needs to support the language.
(syntactic) sublanguage of an OMS language interpreting according to a particular logic that targets specific applications or reasoning methods}
Profiles of OWL 2 include OWL 2 EL, OWL 2 QL, OWL 2 RL, OWL 2 DL, and OWL 2 Full.
Profiles typically correspond to sublogics.
query
sentence containing variables that can be instantiated by a substitution
query language
SPARQL, Prolog
There are also general purpose OMS languages, which can express both OMS and quries.
OMS language specifically dedicated to queries
query variable
From an abstract point of view, query variables are just symbols; they are used in a way that they will be substituted using a substitution. Many OMS languages have special notations for (query) variables.
If there are no variables in an OMS language, constants can be used as query variables.
Usually, query variables are the free variables of a sentence, whereas there can be other (bound) variables.
symbol that will be used in a query and a substitution
refinement
OMS mapping that postulates a specialization relation between two OMS along a morphism between their signatures
refinement
resource
Familiar examples include an electronic document, an image, a source of information with a consistent purpose (e.g., 'today's weather report for Los Angeles'), a service (e.g., an HTTP-to-SMS gateway), and a collection of other resources. A resource is not necessarily accessible via the Internet; e.g., human beings, corporations, and bound books in a library can also be resources. Likewise, abstract concepts can be resources, such as the operators and operands of a mathematical equation, the types of a relationship (e.g., 'parent' or 'employee'), or numeric values (e.g., zero, one, and infinity). \nisref{IETF/RFC 3986:2005, Section 1.1}
IETF/RFC 3986:2005, Section 1.1 deliberately defines a resource as 'in a general sense whatever might be identified by an IRI'. The original source refers to URIs, but DOL uses the compatible IRI standard IETF/RFC 3987:2005 for identification.
something that can be globally identified
satisfaction relation
relation between realizations and sentences indicating which sentences hold true in the realization
satisfiable OMS
OMS that is satisfied by least one realization
semantic domain
mathematically-defined set of values that can represent the intended meanings of language constructs
semantic entity
entity that is of semantic nature, i.e. relating linguistic objects with their semantic denotation in a mathematical structure
semantic rule
specification of a mapping from abstract syntax to a semantic domain
sentence
A sentence can conform to one or more signatures (namely those signatures containing all non-logical symbols used in the sentence).
In a realization, on the one hand, a sentence is always true or false. In an OMS, on the other hand, a sentence can have several logical statuses: it can be an axiom, if postulated to be true; a theorem, if proven from other axioms and theorems; a conjecture, if expecting to be proven from other axioms and theorems; or have another of many possible statuses.
It is quite common that sentences are required to be closed (i.e., have no free variables). However, this depends on the OMS language at hand.
a sentence in an OMS
term that is either true or false in a given realization, i.e., which is assigned a truth value in this realization
sequence
sequence is used here in the sense of syntactic sequence
ordered collection where also multiplicity of elements matters
sequence of correspondences
sequence is used here in the sense of syntactic sequence
sequence whose members are correspondences
sequence of OMS
sequence is used here in the sense of syntactic sequence
sequence whose members are OMS
OMS serialization
Common Logic uses the term 'dialect'; the following are standard Common Logic dialects: Common Logic Interchange Format (CLIF), Conceptual Graph Interchange Format (GCIF), eXtended Common Logic Markup Language (XCL).
OWL uses the term 'serialization' the following are standard OWL serializations: OWL functional-style syntax, OWL/XML, OWL Manchester syntax, plus any standard serialization of RDF (e.g., RDF/XML, Turtle, ...). However, RDF/XML is the only one tools are required to implement.
Serializations serve as standard formats for exchanging OMS between tools.
a serialization of an language
specific syntactic encoding of a given OMS language
synonymous to 'concrete syntax'
set
collection whose members have a certain type, as specified by the type parameter
set of annotation expressions
set whose members are annotation expressions
set of mappings
set whose members are mappings
set of non-logical symbols
set whose members are non-logical symbols
set of sentences
set whose members are sentences
signature
The signature of a term is the set of all non-logical symbols occuring in the term. The signature of an OMS language is the set of all non-logical symbols possible in that language.
set (or otherwise structured entity) of non-logical symbols of an OMS
signature morphism
A list of symbol map items induces a signature morphism.
mapping between two signatures, preserving the structure of the source signature within the target signature
simple theoroidal mapping
true
logic mapping that maps signatures of the source logic to theories of the target logic
orthogonal to WeaklyExactMapping and FaithfulMapping
the resulting theory tpyically contains infrastructure axioms that are needed for expressing the logic mapping
1
reifies property isSimplyTheoroidallyMappableTo
Developers' note: Protégé 4.2 doesn't like 'Class: OMSMapping DisjointUnionOf: PlainMapping, SimpleTheoroidalMapping', so we do it this way:
specification
formal representation of (requirements of) a data structure, an algorithm or a hardware or software system used in systems analysis, requirements analysis and systems design
standoff markup
way of providing annotations to subjects in external resources, without embedding them into the original resource (here: OMS)
structured OMS
OMS that results from other OMS by import, union, combination, renaming or other structuring operations
structuring language aspect
the (unique) language aspect of an OMS language that covers structured OMS as well as the relations of basic OMS and structured OMS to each other, including, but not limited to imports, OMS mappings, conservative extensions, and the handling of prefixes for CURIEs
sublogic
logic embedding that is 'syntactic' in the sense that signature and sentence translations are inclusions
1
reifies property isSubLogicOf
substitution
OMS mapping that maps variables of one OMS to complex terms of another OMS
supports relation
There is also a supports relation between OMS languages and serializations, and one between language mappings and logic mappings.
relation between OMS languages and logics expressing the logical language aspect of the former, namely that the constructs of the former lead to a logical theory in the latter
1
reifies properties: supportsLogic, supportsLogicMapping, supportsSerialization
symbol map item
A symbol map item is given as s_1 |-> s_2, where $s_1$ is a symbol from the source OMS and $s_2$ is a symbol from the target of the OMS mapping.
pair of symbols of two OMS, indicating how a symbol from the first OMS is mapped by a signature morphism to a symbol of the second OMS
term
syntactic expression either consisting of a single non-logical symbol or recursively composed of other terms (a.k.a. its subterms) and possibly logical symbols
theorem prover
software tool implementing theorem proving
theorem proving
process of demonstraing that a sentence (or OMS) is the logical consequence of some OMS
theorem
sentence that has been proven from other axioms and theorems
tool
software for processing DOL libraries and OMS
translation (process)
process of applying a language or logic translation, or flattening an OMS translation
union
structured OMS expressing the combination of all symbols and axioms (and more general constraints) of a sequence of OMS
unsatisfiable OMS
OMS that is not satisfied by any realization
view
When an interpretation is given as a set of correspondences, these are given as tuples, where the type of relationship is given by the specific kind of interpretation.
An interpretation typically leads to proof obligations, \ie one has to prove that axioms of the source OMS of the mapping are theorems in the target OMS.
OMS mapping that postulates a relation between two OMS
a view (also called interpretation) between two heterogeneous OMS in a DOL library
interpretation
weak definitional extension
An extension O_2 of an OMS O_1 is a weak definitional extension, if each realization of O_1 can be expanded to at most one realization of O_2.
extension whose newly introduced non-logical symbols can be interpreted in at most one way
weak definitional extension mapping
An extension O_2 of an OMS O_1 is a weak definitional extension, if each realization of O_1 can be expanded to at most one realization of O_2.
An extension is definitional if and only if it is both weakly definitional and model-theoretically conservative.
mapping of a weak definitional extension
1
reifies property isWeakDefinitionalExtensionOf
weakly exact mapping
true
logic mapping that is weakly compatible with certain DOL structuring constructs
1
reifies property isWeaklyExactlyMappableTo
web entity
entity that is related to the world wide web
Distributed Ontology, Model and Specification Language
When viewed as an OMS language, DOL has OMS as its non-logical symbols, and OMS mappings as its sentences.
unified metalanguage for the structured and heterogeneous expression of ontologies, specifications, and models, using DOL libraries of OMS, OMS mappings and OMS networks