Modelling and Mining Knowledge about Computational Complexity

We present an ontology of computational complexity that allows for a representation of research findings on the subject and supports query answering and reasoning tasks to help students and researchers in finding known facts and deriving new ones. The facts about decision problems and complexity classes are organised as a knowledge graph. The relationships between them are axiomatised using the FOWL framework that allows one to combine OWL 2 and first-order logic to balance between reasoning efficiency and expressive power. While the axioms were created through ontological analysis based on received 'textbook knowledge', the facts were extracted from the textual corpus of the 'Complexity Zoo' website, a human-curated 'encyclopedia' of complexity classes, in a human-supervised process employing large language models. We discuss, on the one hand, the modelling choices in relation to the previous work on knowledge representation in mathematics and, on the other hand, the peculiarities of using language models for the mining of complex symbolic facts. Finally, we illustrate some of the features of the hybrid reasoning system by providing a usage example.