Thursday 17 February 2022, 10:30 AM, room 3U47 and online: A Framework for Proving Ontology-Relations and Testing Ontology Instances, Burkhart Wolff (LMF, Université Paris-Saclay).

Joint work with Idir Ait-Sadoune and Nicolas Méric

Isabelle/DOF is a novel ontology framework on top of Isabelle. Isabelle/DOF allows for the formal development of ontologies as well as continuous checking that a formal document under development conforms to an underlying ontology. Such a document may contain text and code elements as well as formal Isabelle definitions and proofs. Thus, Isabelle/DOF is designed to annotate and interact with typed meta-data within formal developments in Isabelle.

While prior versions of Isabelle/DOF provided already a mechanism to check ontological rules (in OWL terminology) or class invariants (in UML/OCL terminology) via hand- written SML test-code, we provide in this paper a novel mechanism to specify invariants in HOL via a reflection mechanism. This allows for both efficient run-time checking of abstract properties of formal content as well as formal proofs that establish relations between different ontologies in general and specific ontology instances in concrete cases. This concept is also called ontology alignment in the literature raised a substantial interest recently. The mechanism can be used to annotate terms and proof-terms with metas-data.