Ontology engineering

Mahdi Bu Ali

Mahdi Bu Ali completed his MSc in Computer Science at KAUST in 2025 under the supervision of Robert Hoehndorf. His research lay at the intersection of formal mathematics, automated theorem proving, and large language models. His thesis, Automated Theorem Proving with Large Language Models in Lean: An Exploration of Specialized In-Context Learning and General-Purpose Hierarchical Architectures, addresses the long-standing goal of automating mathematical reasoning in interactive theorem provers such as Lean. Automated theorem proving is constrained both by the cost of exploring vast proof search

Safana Bakheet

Safana Bakheet completed her MSc in Bioengineering at KAUST in 2025 under the supervision of Robert Hoehndorf. Her work was carried out in collaboration with Fernando Zhapa-Camacho and developed methods for prioritising disease-causing genes by combining ontology-based phenotype representations with supervised knowledge graph embeddings. Her thesis, An Inductive, Supervised Gene-Disease Associations Method, introduces a ranking model that scores candidate disease-causing genes based on the similarity of their associated phenotypes, represented in the Mammalian Phenotype Ontology (MP) and the

Md Nurul Muttakin

Md Nurul Muttakin completed his MSc in Computer Science at KAUST in 2023 under the supervision of Robert Hoehndorf. His research focused on machine learning methods for predicting protein function from three-dimensional structural information. His thesis, 3D conformation-based protein function prediction, investigated how structural information should be exploited by deep learning models in light of the availability of near-experimental-accuracy structures from AlphaFold. Almost all existing structure-aware protein function predictors combine graph neural networks (GNNs) operating on 2D

Knowledge Representation and Reasoning (2015-2016)

Year: 2015-2016 Code: CS 213 Program: Computer Science Institution: KAUST Role: Instructor Topics: Ontology engineering, Applied Ontology

Applied Ontology (2016-2017)

Year: 2016-2017 Code: CS 390EE Program: Computer Science Institution: KAUST Role: Instructor Topics: Applied Ontology, Ontology engineering

Knowledge Representation and Reasoning (2017-2018)

Year: 2017-2018 Code: CS 213 Program: Computer Science Institution: KAUST Role: Instructor Topics: Ontology engineering, Applied Ontology

Applied Ontology (2018)

Year: 2018 Code: CS 322 Program: Computer Science Institution: KAUST Role: Instructor Topics: Applied Ontology, Ontology engineering

Knowledge Representation and Reasoning (2020)

Year: 2020 Code: CS 213 Program: Computer Science Institution: KAUST Role: Instructor Topics: Ontology engineering, Applied Ontology, Neuro-symbolic AI

Knowledge Representation and Reasoning (2021)

Year: 2021 Code: CS 213 Program: Computer Science Institution: KAUST Role: Instructor Topics: Ontology engineering, Applied Ontology, Neuro-symbolic AI

Knowledge Representation and Reasoning (2022)

Year: 2022 Code: CS 213 Program: Computer Science Institution: KAUST Role: Instructor Topics: Ontology engineering, Applied Ontology, Neuro-symbolic AI

Knowledge Representation and Reasoning (2024)

Year: 2024 Code: CS 213 Program: Computer Science Institution: KAUST Role: Instructor Topics: Ontology engineering, Applied Ontology, Neuro-symbolic AI

Knowledge Representation and Reasoning (2026)

Year: 2026 Code: CS 213 Program: Computer Science Institution: KAUST Role: Instructor Topics: Ontology engineering, Applied Ontology, Neuro-symbolic AI
crg explainable ml ontologies

Towards sound, complete, and explainable machine learning with biomedical ontologies (CRG11)

Deep learning has driven much of the recent progress in bioinformatics, but the resulting models are essentially black boxes: it is hard or impossible to ask why a prediction was made, to verify it against existing knowledge, or to detect biases that emerge from the interaction of dataset, architecture, and training objective. In clinical and biomedical settings these limitations matter, both because clinicians need to trust the systems they use and because formal guarantees of soundness and fairness can only be obtained when the inferential machinery can be inspected. The grand challenge