Skip to main content

Logical Methods research group

As the group's name suggests, we are interested in developing and applying symbolic logic formalisms to represent, analyse and query data, knowledge and computations. The Logical Methods group has three main clusters of expertise:

Knowledge representation, knowledge graphs, logic-based AI: We investigate, develop and utilise logical formalisms for encoding general knowledge about application domains, which allows information systems to derive new information from data. Our concern is striking a practically acceptable balance between the expressive power of a formalism and the computational complexity of reasoning with it, as well as designing and implementing optimal reasoning algorithms. In particular, we are interested in temporal and spatial representation and reasoning, ontology and query languages for knowledge graphs, semantic web and ontology-based data access. For example, our work has contributed to the theory and applications of ontology-based data access with OWL2QL ontologies and their temporal extensions, including query answering algorithms and the development of the leading virtual knowledge graph system Ontop.

Graph data modelling: Our primary research focus is on representing, querying, and analysing graph-shaped data at scale. Our work includes data modelling, graph databases and query languages along with their complexity and optimisation challenges. This work includes a leading role in the LDBC (Linked Data Benchmark Council) working group for discussing proposals for the schema language for GQL, which is a query language for Labelled Property Graphs associated with SQL and managed by the ISO ISO/IEC JTC 1/SC 32/WG 3 working group for querying property graphs. An important part of this research is the investigation of the consequences of schema languages for the typing of query languages, which is of use for helping developers to write correct well-typed queries and updates, but also for deriving typing information for the sake of query optimisation. Another part of the research focuses on reasoning over schemas and data mappings for the sake of data integration and data transformation, where it is important to check if certain mappings always produce a graph that conforms to a particular given schema.

Program analysis, verification, software engineering: We develop automated techniques and software tools for modelling, analysis and verification of programs and computer systems and apply them to software engineering. One of our main tools for tackling the inherent search problems is logic-based constraint solving technology, such as SAT and SMT solvers, specifically dedicated solvers for string-manipulating programs. We have expertise in automated analysis of qualitative and quantitative system properties such as termination, time and space complexity, safety and information-flow properties, bisimilarity and equivalence. Apart from software in the main programming paradigms, our objects of analysis include probabilistic and fuzzy systems, neural networks, parallel programs, and rewrite systems. We are working on frontiers including machine learning-empowered software engineering, analysis and verification of deep neural networks, and neural-symbolic systems, with applications to API/code recommendation, source code summarisation, software artefact defect detection, and cryptography.

Group members