dc.contributor.author | Brucker, AD | |
dc.contributor.author | Ait-Sadoune, I | |
dc.contributor.author | Crisafulli, P | |
dc.contributor.author | Wolff, B | |
dc.date.accessioned | 2019-12-09T13:31:11Z | |
dc.date.issued | 2018-07-18 | |
dc.description.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. | en_GB |
dc.identifier.citation | Vol. 11006 LNCS, pp. 23 - 38 . International Conference on Intelligent Computer Mathematics CICM 2018: Intelligent Computer Mathematics | en_GB |
dc.identifier.doi | 10.1007/978-3-319-96812-4_3 | |
dc.identifier.uri | http://hdl.handle.net/10871/40035 | |
dc.language.iso | en | en_GB |
dc.publisher | Springer Verlag (Germany) | en_GB |
dc.rights | © 2018, Springer International Publishing AG, part of Springer Nature. | en_GB |
dc.subject | Ontology | en_GB |
dc.subject | Ontological modeling | en_GB |
dc.subject | Isabelle/DOF | en_GB |
dc.title | Using the isabelle ontology framework: Linking the formal with the informal | en_GB |
dc.type | Conference proceedings | en_GB |
dc.date.available | 2019-12-09T13:31:11Z | |
dc.identifier.isbn | 9783319968117 | |
dc.identifier.issn | 0302-9743 | |
dc.description | This is the author accepted manuscript. The final version is available from the publisher via the DOI in this record | en_GB |
dc.identifier.journal | Lecture Notes in Computer Science | en_GB |
dc.rights.uri | http://www.rioxx.net/licenses/all-rights-reserved | en_GB |
dcterms.dateAccepted | 2018-07-18 | |
rioxxterms.version | AM | en_GB |
rioxxterms.licenseref.startdate | 2018-07-18 | |
rioxxterms.type | Conference Paper/Proceeding/Abstract | en_GB |
refterms.dateFCD | 2019-12-09T13:29:52Z | |
refterms.versionFCD | AM | |
refterms.dateFOA | 2019-12-09T13:31:15Z | |
refterms.panel | B | en_GB |