by Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart Wolff
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 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.
Keywords: Isabelle/Isar, HOL, Ontologies
Categories: ,
Documents: (full text as PDF file)
Please cite this article as follows:
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 (11006), Springer-Verlag, 2018.
Keywords: Isabelle/Isar, HOL, Ontologies
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-319-96812-4_3) (
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}, | |
= | {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}, |