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 Raw Permalink Blame History

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