Using the Isabelle Ontology Framework: Linking the Formal with the Informal

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

Please cite this work as follows:
A. D. Brucker, I. Ait-Sadoune, P. Crisafulli, and B. Wolff, “Using the Isabelle ontology framework: Linking the formal with the informal,” in Conference on intelligent computer mathematics (CICM), Heidelberg: Springer-Verlag, 2018. doi: 10.1007/978-3-319-96812-4_3. Author copy: http://logicalhacking.com/publications/brucker.ea-isabelle-ontologies-2018/

BibTeX
@InCollection{ brucker.ea:isabelle-ontologies:2018,
  keywords  = {Isabelle/Isar, HOL, Ontologies},
  location  = {Hagenberg, Austria},
  author    = {Achim D. Brucker and Idir Ait-Sadoune and Paolo Crisafulli
               and Burkhart Wolff},
  booktitle = {Conference on Intelligent Computer Mathematics (CICM)},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {11006},
  title     = {Using the {Isabelle} Ontology Framework: Linking the Formal
               with the Informal},
  areas     = {formal methods, software},
  year      = {2018},
  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.},
  note      = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-isabelle-ontologies-2018/}},
}