An Ontology Framework for Formal Libraries
Vendredi 12 juillet 2024 à 13:30h, Batiment 650, 435 (Salle des Theses).
Abstract.
Document ontologies, i. e., a machine-readable form of the structure of documents as well as the document discourse, play a key role in structuring the link between semantic notions and documents containing infor- mal text. In many scientific disciplines such as medicine or biology, ontologies allows the organization of research papers and their automated access. There are particular challenges in the field mathematics and engineering where documents contain both formal and informal text- elements with a complex structure of mutual links and dependencies of various types. Texts may contain formulas (which should be at least type-correct and if possible semantically consistent with the formal definitions) and formal definitions based on naming conventions that should reflect informal explanations. A deeper access into the formal parts of this type of documents involves a framework that can cope with typed, logical languages, which requires going substantially further than existing ontological languages like, for example, OWL.
The starting point of this work was the ontological language ODL implemented in Isabelle/DOF. Deeply integrated into the interactive theorem proving system Isabelle/HOL and its front-end PIDE, it allows both the development of typed ontologies and of documents containing definitions, documentation, and formal proofs. The ontologies gen- erate theories of meta-data and use them for the validation of constraints which were enforced during document editing. The original implementation supported links to terms in definitions and proofs, but not links between terms, nor the addition of structured meta-information inside and between formulas or proofs. The validation mechanisms for meta-information were limited to hand-crafted solutions. Furthermore, formal entities like definitions or lemmas could not be referenced as ontological entities. These features are nevertheless essential for a number of applications when it comes to the exchange of (semi-)formal information between interactive and automated provers on the one hand and to advanced “semantic”, knowledge- oriented search techniques in these documents on the other hand.
This thesis overcomes these limitations: Isabelle/DOF is extended by a description and an evaluation mechanism of meta-information inside the level of terms and proof-objects. It is therefore designed to provide a “deeper” integration into formal mathematical library texts, where formal entities can be abstracted and become document elements. Formal entities representing terms, definitions or theorems can be referenced and used as first class ontological objects. The new support of type classes parameterized polymorphism allows to generalize ontological concepts. These new features in Isabelle/DOF can express not only links between informal text and formal ontological concepts but also between formal or informal entities as elements of a document, thus improving the linking between document elements and knowledge in mathematical and engineering texts. A reification mechanism in Isabelle/DOF allows to attach ontological meta-data to proof objects to add knowledge about the structure of the proof scripts and associated proof tactics used to prove a theorem. It should be relevant for import/export techniques of proofs between theorem provers.
My manuscript is available here.
Membres du jury :
- Dominique MERY, Professeur, LORIA Nancy, Université de Lorraine - Rapporteur & Examinateur
- Yamine AïT-AMEUR, Professeur, ENSEEIHT-Toulouse, Université de Toulouse - Rapporteure & Examinatrice
- Frédéric BOULANGER, Professeur, CentraleSupélec, Université Paris-Saclay - Examinateur
- Catherine DUBOIS, Professeure, ENSIIE, Université Paris Saclay - Examinatrice
- Régine LALEAU, Professeure, LACL, Université Paris-Est Créteil - Examinatrice
- Laure PETRUCCI, Professeure, LIPN, Université Sorbonne-Paris-Nord - Examinateur
Directeur de thèse : Burkhart Wolff, Directeur de recherche Co-encadrant : Idir Ait-Sadoune