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 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Fluent editor (2018). http://www.cognitum.eu/Semantics/FluentEditor/
The neon toolkit (2018). http://neon-toolkit.org
Ontologies (2018). https://www.w3.org/standards/semanticweb/ontology
Owlgred (2018). http://owlgred.lumii.lv/
Protégé (2018). https://protege.stanford.edu
R language package for fluent editor (rontorion) (2018). http://www.cognitum.eu/semantics/FluentEditor/rOntorionFE.aspx
Adler, J.: R in a Nutshell. O’Reilly, Sebastopol (2010)
Bezzecchi, S., Crisafulli, P., Pichot, C., Wolff, B.: Making agile development processes fit for V-style certification procedures. In: ERTS Conference Proceedings, ERTS 2018 (2018)
Boulanger, J.L.: CENELEC 50128 and IEC 62279 Standards. Wiley-ISTE, Boston (2015). The reference on the standard
Common Criteria: Common criteria for information technology security evaluation (version 3.1), part 3: security assurance components (2006). CCMB-2006-09-003
Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9
Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle/PIDE. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 515–530. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08970-6_33
Wenzel, M.: The Isabelle/Isar reference manual (2017). Part of the Isabelle distribution
Wenzel, M., Wolff, B.: Building formal method tools in the Isabelle/Isar framework. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 352–367. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74591-4_26
Acknowledgement
This work was partly supported by the framework of IRT SystemX, Paris-Saclay, France, and therefore granted with public funds within the scope of the Program “Investissements d’Avenir”.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Brucker, A.D., Ait-Sadoune, I., Crisafulli, P., Wolff, B. (2018). Using the Isabelle Ontology Framework. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds) Intelligent Computer Mathematics. CICM 2018. Lecture Notes in Computer Science(), vol 11006. Springer, Cham. https://doi.org/10.1007/978-3-319-96812-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-96812-4_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-96811-7
Online ISBN: 978-3-319-96812-4
eBook Packages: Computer ScienceComputer Science (R0)