Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Adding a text explaining the interest of the ontology mapping.

This commit is contained in:
Idir AIT SADOUNE 2022-02-03 10:17:33 +01:00
parent 4b43756eb3
commit b0a29ac00d
1 changed files with 19 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
src/tests/Mapped_PILIB_Ontology.thy
View File

@ -3,24 +3,14 @@ theory Mapped_PILIB_Ontology
begin
text\<open>
PLIB does not assume that all data sources use the same ontology.
Each data source may build its local ontology without any external reference.
It may also build it based upon one or several reference ontologies (i. e., standard ones).
A class of a local ontology may be described as subsumed by one or several other class(es) defined in other ontologies.
This means that each instance of the former is also instance of the latter. This relationship is named case-of.
Though case- of relationship the subsumed class may either import properties (their GUI and definitions are preserved)
or map properties (the properties are different but they are semantically equivalent) that are defined in the referenced class(es).
It may also define additional properties.
\<close>
text\<open>
The following example is extract from this reference :
CONTEXT-EXPLICATION IN CONCEPTUAL ONTOLOGIES: PLIB ONTOLOGIES AND THEIR USE FOR INDUSTRIAL DATA
Special issue of JAMS - Journal of Advanced Manufacturing Systems
By GUY PIERRA
\<close>
text\<open>User Ontology\<close>
text\<open>Local Ontology\<close>
onto_class Item =
item_name :: string
@ -76,6 +66,23 @@ onto_class Hardware = Informatic +
onto_class R_Software = Informatic +
version :: int
text\<open>
Isa_DOF framework does not assume that all documents reference the same ontology.
Each document may build its local ontology without any external reference.
It may also build it based upon one or several reference ontologies (i.e., standard ones).
The relationship between the local ontology and the reference one is formalised using a morphism function.
More precisely, a class of a local ontology may be described as a consequence of a transformation applied
to one or several other class(es) defined in other ontologies. This means that each instance of the former can be
computed from one or more instances of the latter.
Thanks to the morphism relationship, the obtained class may either import properties (definitions are preserved)
or map properties (the properties are different but are semantically equivalent) that are defined in the referenced class(es).
It may also define additional properties.
\<close>
definition Item_to_Resource_morphism
where "Item_to_Resource_morphism (\<sigma>::'a Item_scheme) =
\<lparr> tag_attribute = 0::int
@ -92,6 +99,4 @@ definition U_Software_to_R_Software_morphism
\<rparr>"
end