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

updating Idir's part

This commit is contained in:
Idir AIT SADOUNE 2022-02-08 09:40:41 +01:00
parent b9c72124c0
commit 7cd7a4d15d
2 changed files with 10 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
examples/scholarly_paper/2021-ITP-PMTI/paper.thy
View File

@ -912,6 +912,11 @@ To check the coherence of our local ontology, we define a relationship between t
and the reference ontology using morphism functions (or mapping rules). These rules are applied to
define the relationship between one class of the local ontology to one or several other class(es)
described in the reference ontology.
For example,\<open>Product_to_Component_morphism\<close> and \<open>Computer_Hardware_to_Hardware_morphism\<close> definitions,
detailed in the figure Z, specify how \<open>Product\<close> or \<open>Computer_Hardware\<close> objects are mapped to \<open>Component\<close>
or \<open>Hardware\<close> objects defined in the reference ontology. This mapping shows that the structure
of a (user) ontology may be quite different from the one of a standard ontology she references.
\<close>
section*[ontoexample::text_section,main_author="Some(@{docitem ''idir''}::author)"] \<open>Applications\<close>

13
src/tests/Mapped_PILIB_Ontology.thy
View File

@ -124,7 +124,7 @@ definition Product_to_Component_morphism :: "'a Product_scheme \<Rightarrow> Com
where " \<sigma> \<langle>Component\<rangle>\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t = \<lparr> Resource.tag_attribute = 1::int ,
Resource.name = name \<sigma> ,
Electronic.provider = Product.provider \<sigma> ,
Electronic.manufacturer = '''' ,
Electronic.manufacturer = ''no manufacturer'' ,
Component.mass = Product.mass \<sigma> ,
Component.dimensions = [] \<rparr>"
@ -147,13 +147,10 @@ and the reference ontology using morphism functions (or mapping rules). These ru
define the relationship between one class of the local ontology to one or several other class(es)
described in the reference ontology.
For example,
\<close>
text\<open>
As shown by our example, the structure of a (user) ontology may be quite different from the one
of a standard ontology she references.
For example,\<open>Product_to_Component_morphism\<close> and \<open>Computer_Hardware_to_Hardware_morphism\<close> definitions,
detailed in the figure Z, specify how \<open>Product\<close> or \<open>Computer_Hardware\<close> objects are mapped to \<open>Component\<close>
or \<open>Hardware\<close> objects defined in the reference ontology. This mapping shows that the structure
of a (user) ontology may be quite different from the one of a standard ontology she references.
\<close>