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

reviewed critical parts
ci/woodpecker/push/build Pipeline was successful Details 

- introction: ITP explained
- revised related work
- revised conclusion
This commit is contained in:
Burkhart Wolff 2022-04-25 21:16:12 +02:00
parent 1714703272
commit fbf34f9a35
1 changed files with 11 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -254,10 +254,10 @@ for advanced queries of elements inside an integrated source, and invariants
allow for formal proofs over the relations/translations of ontologies and ontology-instances. allow for formal proofs over the relations/translations of ontologies and ontology-instances.
The latter question raised scientific interest under the label ``ontology mapping'' for The latter question raised scientific interest under the label ``ontology mapping'' for
which we therefore present a formal solution. To sum up, we completed \<^dof> to which we therefore present a formal solution. To sum up, we completed \<^dof> to
a fairly rich, ITP-oriented ontology language, which is a concrete proposal for formal a fairly rich ontology language oriented to interactive theorem proving (ITP) systems,
development projects targeting a certification, for technical documentation or books which is a concrete proposal for formal development projects targeting a certification,
with a high amount of machine-checked formal content or for mathematical libraries for technical documentation, for books with a high amount of machine-checked formal content
such as the AFP.\<close> or for mathematical libraries such as the AFP.\<close>
(*<*) (*<*)
declare_reference*[casestudy::text_section] declare_reference*[casestudy::text_section]
@ -1160,16 +1160,16 @@ that allows users to introduce their own category concepts.
Both suffer from the lack of deeper meta-data modeling, and the latter is still at the beginning Both suffer from the lack of deeper meta-data modeling, and the latter is still at the beginning
(ScienceWISE marks the Mathematics part as ``under construction''). (ScienceWISE marks the Mathematics part as ``under construction'').
Regarding using formal methods to formalise standards, Event-B method was used by Regarding the use of formal methods to formalise standards, the Event-B method was proposed by
Fotso et al. @{cite "FotsoFLM18"} to propose a specification of the hybrid ERTMS/ETCS level 3 standard, Fotso et al. @{cite "FotsoFLM18"} for specifications of the hybrid ERTMS/ETCS level 3 standard,
in which requirements are specified using SysML/KAOS goal diagrams that are translated into in which requirements are specified using SysML/KAOS goal diagrams. The latter were translated into
Event-B, and domain-specific properties are specified by ontologies. Event-B, where domain-specific properties were specified by ontologies.
In another case, Mendil et al. @{cite "MendilASMP21"} propose an Event-B framework for formalising standard In another case, Mendil et al. @{cite "MendilASMP21"} propose an Event-B framework for formalising standard
conformance through formal modelling of standards as ontologies. conformance through formal modelling of standards as ontologies.
The proposed approach was exemplified on ARINC 661 standard and weather radar system application. The proposed approach was exemplified on ARINC 661 standard im the ntext of a weather radar system application.
These works are essentially interested in expressing ontological concepts in a formal method These works are essentially interested in expressing ontological concepts in a formal method
but do not explicitly deal with the formalisation of rules/invariants defined in ontologies but do not explicitly deal with the formalisation of rules/invariants defined in ontologies.
and are not interested in the question of mapping ontologies. The question of ontology-mappings is not addressed.
% \<^url>\<open>https://github.com/CLLKazan/OntoMathPro\<close> % \<^url>\<open>https://github.com/CLLKazan/OntoMathPro\<close>
% %