forked from Isabelle_DOF/Isabelle_DOF
Un update of the PLIB example
This commit is contained in:
parent
f8c125bcff
commit
4936a8142e
|
@ -3,6 +3,23 @@ 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>
|
||||
|
||||
onto_class Item =
|
||||
|
@ -74,4 +91,7 @@ definition U_Software_to_R_Software_morphism
|
|||
, version = U_Software.version \<sigma>
|
||||
\<rparr>"
|
||||
|
||||
|
||||
|
||||
|
||||
end
|
Reference in New Issue