added (incomplete) ref to ABZ paper
This commit is contained in:
parent
91ff9c67af
commit
25473b177b
|
@ -73,6 +73,33 @@
|
|||
public = {yes}
|
||||
}
|
||||
|
||||
@InCollection{ brucker.ea:deep-ontologies:2023,
|
||||
author = {Achim D. Brucker and Idir Ait-Sadoune and Nicolas Meric and Burkhart Wolff},
|
||||
booktitle = {9th International Conference on Rigorous State-Based Methods (ABZ 2023)},
|
||||
language = {USenglish},
|
||||
publisher = {Springer-Verlag},
|
||||
address = {Heidelberg},
|
||||
series = {Lecture Notes in Computer Science},
|
||||
number = {XXXXX},
|
||||
title = {{U}sing {D}eep {O}ntologies in {F}ormal {S}oftware {E}ngineering},
|
||||
year = {2023},
|
||||
abstract = {Isabelle/DOF is an ontology framework on top of Isabelle Isabelle/DOF allows for the
|
||||
formal development of ontologies as well as continuous conformity-checking of
|
||||
integrated documents annotated by ontological data. An integrated document may
|
||||
contain text, code, definitions, proofs and user-programmed constructs supporting a
|
||||
wide range of Formal Methods. Isabelle/DOF is designed to leverage traceability in
|
||||
integrated documents by supporting navigation in Isabelle’s IDE as well as the
|
||||
document generation process.
|
||||
In this paper we extend Isabelle/DOF with annotations of terms, a pervasive
|
||||
data-structure underlying Isabelle used to syntactically rep- resent expressions
|
||||
and formulas. Rather than introducing an own pro- gramming language for meta-data,
|
||||
we use Higher-order Logic (HOL) for expressions, data-constraints, ontological
|
||||
invariants, and queries via code-generation and reflection. This allows both for
|
||||
powerful query languages and logical reasoning over ontologies in, for example,
|
||||
ontological mappings. Our application examples cover documents targeting formal
|
||||
certifications such as CENELEC, Common Criteria, etc.}
|
||||
}
|
||||
|
||||
@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
|
||||
|
|
Loading…
Reference in New Issue