Logical Methods
We develop and apply symbolic logic formalisms to represent, analyse and query data, knowledge and computations. Our research ranges from tackling fundamental problems to informing international standards for ontology and query languages, and to designing and implementing practical algorithms and tools for real-world applications.
Databases and Knowledge Representation Group
This group works on logic-based AI and graph data modelling.
In logic-based AI, we investigate and utilise logical formalisms for ontology and query languages in knowledge graphs, ontology-based data access, and temporal and spatial representation and reasoning. Our work has contributed to theory and applications of OWL2QL ontologies standardised by W3C and their temporal extensions, including query answering algorithms and the development of the leading virtual knowledge graph system Ontop.
In graph data modelling, we focus on representing, querying and analysing graph-shaped data at scale. Our work includes data modelling, graph databases and query languages with their complexity and optimisation challenges. We play a leading role in the Linked Data Benchmark Council working group, which oversees the schema language for Graph Query Language GQL standardised and managed by ISO/IEC.
Group members
- Jan Hidders. Research interests: Graph databases, graph indexing, graph query languages, graph schema languages, graph analytics, JSON query languages, JSON schema languages, conceptual data modelling, data integration, fact-based modelling. Jan's DBLP profile. Jan's Google Scholar profile.
- Roman Kontchakov. Research interests: Knowledge representation and reasoning, description logic, spatial logic, semantic web. Roman's DBLP profile. Roman's Google Scholar profile.
- Vladislav Ryzhikov. Research interests: Knowledge representation and reasoning, temporal and spatial data, temporal logics, semantic web, description logics, conceptual modelling. Vladislav's DBLP profile. Vladislav's Google Scholar profile.
- Peter Wood. Research interests: Data management, data querying, query optimisation, rule languages, graph databases. Peter's DBLP profile. Peter's Google Scholar profile.
- Michael Zakharyaschev. Research interests: Knowledge representation and reasoning, logic, ontology-based data access, semantic web. Michael's DBLP profile. Michael's Google Scholar profile.
Verification and Software Engineering Group
This group develops automated techniques and tools for the modelling, analysis and verification of programs and computer systems and applies them to software engineering. Our work includes analysis of string-manipulating programs based on constraint-solving and analysis of program termination and time/space complexity based on term-rewriting. We have also made strong contributions in emerging areas of neuro-symbolic software engineering and verification.
- Carsten Fuhs (Group Lead). Research interests: Automated program analysis and verification (termination, time complexity bounds, safety, equivalence), term rewriting, SAT and SMT solving, separation logic. Carsten's DBLP profile. Carsten's Google Scholar profile.
- Taolue Chen. Research interests: AI (machine learning and natural language processing) for software sciences, neuro-symbolic software engineering, program analysis and verification. Taolue's DBLP profile. Taolue's Google Scholar profile.
- Tingting Han. Research interests: Formal verification, synthesis of probabilistic systems and its applications. Tingting's DBLP profile. Tingting's Google Scholar profile.