forked from Isabelle_DOF/Isabelle_DOF
updating proving morphisms on ontologies section
This commit is contained in:
parent
76cff5beab
commit
acbaa582ef
|
@ -988,10 +988,7 @@ This mapping shows that the structure of a (user) ontology may be arbitrarily di
|
||||||
from the one of a standard ontology it references.
|
from the one of a standard ontology it references.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text\<open>
|
|
||||||
The advantage of using the \<^dof> framework compared to approaches like ATL or EXPRESS-X is
|
|
||||||
the possibility of formally verifying the \<^emph>\<open>mapping rules\<close>. \<^ie> proving the preservation
|
|
||||||
of invariants, as we will demonstrate in the following example.\<close>
|
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
\begin{figure}
|
\begin{figure}
|
||||||
|
@ -1013,8 +1010,10 @@ lemma Computer_Hardware_to_Hardware_morphism_total :
|
||||||
\<close>
|
\<close>
|
||||||
text\<open>The example proof in \autoref{fig-xxx} for a simple, but typical example of reformatting
|
text\<open>The example proof in \autoref{fig-xxx} for a simple, but typical example of reformatting
|
||||||
meta-data into another format along an ontological mapping are nearly trivial: after unfolding
|
meta-data into another format along an ontological mapping are nearly trivial: after unfolding
|
||||||
the invariant and the morphism definitions, the preservation proof is automatic.
|
the invariant and the morphism definitions, the preservation proof is automatic. The advantage
|
||||||
\<close>
|
of using the \<^dof> framework compared to approaches like ATL or EXPRESS-X is
|
||||||
|
the possibility of formally verifying the \<^emph>\<open>mapping rules\<close>. \<^ie> proving the preservation
|
||||||
|
of invariants, as we will demonstrate in the following example.\<close>
|
||||||
|
|
||||||
(*
|
(*
|
||||||
section*[ontoexample::text_section,main_author="Some(@{docitem ''idir''}::author)"]
|
section*[ontoexample::text_section,main_author="Some(@{docitem ''idir''}::author)"]
|
||||||
|
|
Reference in New Issue