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

Merge remote-tracking branch 'refs/remotes/origin/ICFEM-2022' into ICFEM-2022
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2022-04-20 14:58:15 +02:00
parent 35b50e419f 230336f0a4
commit 57c984d4dc
1 changed files with 3 additions and 2 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

@ -254,8 +254,9 @@ for advanced queries of elements inside an integrated source, and invariants
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
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 the
ITP community allowing a deeper structuring of mathematical libraries
a fairly rich, ITP-oriented ontology language, which is a concrete proposal for formal
development projects targeting a certification, for technical documentation or books
with a high amount of machine-checked formal content or for mathematical libraries
such as the AFP.\<close>
(*<*)