Logic has long been considered the midwife of computer science. From Church and Turing's revolutionary ideas to the AI systems we use every day, logic thinking shapes everything about how computers work. We view logic as a fundamental discipline and the basis for practical applications that shape our digital world.
Logic is the language of reason that allows us to move from premise to conclusion with certainty. The mathematical foundation underpinning everything from simple computer programs to sophisticated AI systems, it provides the rigorous methods we need to verify our digital world works as intended.
UCL Computer Science’s Logic research sits at the intersection of philosophy, mathematics and computing.
Where is our research taking us at UCL Computer Science?
Our work spans everything from abstract mathematical theories to everyday tools used by the world's largest tech companies.
Building the foundations of meaning and reasoning
We’re showing the world the way forward with research into inferentialism and proof-theoretic semantics to better understand how meaning comes from use rather than abstract definitions.
While that might sound theoretical, it's incredibly practical as it helps us understand everything from programming languages to human conversation, giving us a clearer picture of how information becomes meaningful when people and systems interact.
Our research is recognised as one of the strongest in the world, particularly through our pioneering work in 'proof-theoretic semantics' – a logical realisation of ‘inferentialism’. This philosophical approach grounds language meaning in how it's used rather than what it represents, creating powerful new frameworks for understanding both human and machine communication.
Natural language semantics
Traditionally, logic and probability theory belong to different areas of mathematics and are often studied in separate university departments. But solving real-world problems requires methods from both fields. Our researchers are developing unified mathematical models for natural language that can reason with both logic and statistics.
While the rules of syntax – like grammar – are logical, the rules of semantics follow statistical patterns. It's these statistical patterns that machine learning can discover and that have made large language models (LLMs) so successful. We're working with logical systems that encode grammatical rules and developing statistical semantics for them, using approaches like the Lambek Calculus and sheaf theory to bridge these traditionally separate mathematical worlds.
One advantage of this research is that it generates mathematical objects – like tensors – that quantum computers can learn, connecting our work with the emerging field of quantum computing.
Proving software correct
Our researchers have developed verification tools now used by Meta and Amazon Web Services (AWS) to analyse and secure critical software. In fact, UCL spinout companies and industry collaborations are turning academic theories into practical tools that identify bugs and security vulnerabilities before they impact billions of users.
This verification work extends to AI systems, where our logical approaches help create more explainable and transparent algorithms. And as AI reaches into all parts of society, our research is making these systems accountable and understandable to the people using them.
Semantics for computation and programming languages
Supported by the Advanced Research and Invention Agency (ARIA) and the Engineering and Physical Sciences Research Council (EPSRC), we’re developing formal methods to better understand key computational models used in AI, including in areas such as Bayesian inference, learning algorithms and AI-assisted organic molecule design.
The aim? To establish rigorous mathematical foundations that make AI systems easier to interpret, more reliable, and simpler to test for errors – so future AI is both expressive and trustworthy.
Cross-disciplinary collaboration
What makes our work special is how we bring different fields together. We don't just stay in our academic lanes – we connect centuries-old philosophical logic with today's computational methods to build bridges across disciplines that have traditionally worked separately.
For example, we're currently establishing UCL LILAC (Logic, Information, Language, and Computation). This research group will bring together researchers from Engineering Sciences, Arts and Humanities and Language and Brain Sciences to create a London counterpart to Amsterdam's renowned Institute for Logic, Language and Computation.
What's coming next?
Many people worry about AI systems that can't explain their decisions. We’re tackling this head-on by developing the foundations for more transparent technology. For example, our work in explainable AI and formal verification is helping to create advanced trustworthy systems that can show their workings and justify their decisions.
Through our research, industry partnerships and educational programmes – including our forthcoming BA in Philosophy and Computer Science (offered by UCL Philosophy) – we’re making sure that tomorrow's intelligent systems are built on solid logical foundations that reflect human values and reasoning.
