Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting as well as formal development.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

42 lines
2.4 KiB

  1. To cite Isabelle/DOF in publications, please use
  2. Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart
  3. Wolff. Using The Isabelle Ontology Framework: Linking the Formal
  4. with the Informal. In Conference on Intelligent Computer Mathematics
  5. (CICM). Lecture Notes in Computer Science, Springer-Verlag, 2018.
  6. A BibTeX entry for LaTeX users is
  7. @InCollection{ brucker.ea:isabelle-ontologies:2018,
  8. abstract = {While Isabelle is mostly known as part of Isabelle/HOL (an
  9. interactive theorem prover), it actually provides a framework
  10. for developing a wide spectrum of applications. A particular
  11. strength of the Isabelle framework is the combination of text
  12. editing, formal verification, and code generation.\\\\
  13. Up to now, Isabelle's document preparation system lacks a mechanism
  14. for ensuring the structure of different document types (as, e.g.,
  15. required in certification processes) in general and, in particular,
  16. mechanism for linking informal and formal parts of a document.\\\\
  17. In this paper, we present Isabelle/DOF, a novel Document Ontology
  18. Framework on top of Isabelle. Isabelle/DOF allows for conventional
  19. typesetting \emph{as well} as formal development. We show how to model
  20. document ontologies inside Isabelle/DOF, how to use the resulting
  21. meta-information for enforcing a certain document structure, and discuss
  22. ontology-specific IDE support.},
  23. address = {Heidelberg},
  24. author = {Achim D. Brucker and Idir Ait-Sadoune and Paolo Crisafulli and Burkhart Wolff},
  25. booktitle = {Conference on Intelligent Computer Mathematics (CICM)},
  26. doi = {10.1007/978-3-319-96812-4_3},
  27. keywords = {Isabelle/Isar, HOL, Ontologies},
  28. language = {USenglish},
  29. location = {Hagenberg, Austria},
  30. number = {11006},
  31. pdf = {},
  32. publisher = {Springer-Verlag},
  33. series = {Lecture Notes in Computer Science},
  34. title = {Using the {Isabelle} Ontology Framework: Linking the Formal with the Informal},
  35. url = {},
  36. year = {2018},
  37. }