Alex Hyman offered a studentship to start a PhD in Artificial Intelligence
Congratulations to Alex Hyman, who has been offered a full studentship to do a PhD in Artificial Intelligence. He will be joining AIML in September 2025.
news
New pre-print on understanding the activities of older adults via logic and data
In this work, we introduce a framework for representing and reasoning about the Activities of Daily Living of older adults living independently at home. The framework integrates data from sensors and contextual information that aggregates semi-structured interviews, home layouts and sociological observations from the participants.
Pre-print: arXiv:2507.08701.
James Vaughan passes his PhD viva
Congratulations to James Vaughan who has passed his PhD viva with minor corrections. His thesis was on “Adaptable Latent Semantics for Automated Reasoning in Large Theories” and his examiners were Alexander Bolotov (University of Westminster) and Paul Jackson (Edinburgh).
The Royal Society Disability Technology report is out
The Disability Technology report, which explores the potential for data-driven digital technologies to reduce barriers that disabled people encounter in their everyday lives, was launched on the 23rd of June at the Royal Society.
The report’s steering committee included Professor Sir Bernard Silverman FRS (Chair), Dr Vint Cerf FRS, Professor Jacques Fleuriot, Dr Hamied Haroon, Dr Louise Hickman, Professor Catherine Holloway, Prateek Madhav, Professor Paul Upchurch, Professor Seralynne Vann and Professor Mike Wald.
Additional information:
- The link to the audio format of the report is at: https://www.youtube.com/playlist?list=PLg7f-TkW11iVSYxrcd1ReCAo3Iu8A-3Tf.
- A recording of the launch event can be found at: https://www.youtube.com/watch?v=aoFYnEwWFjE.
Our new paper on chronic illnesses and depression featured in UKRI news
Our new paper, Cluster and survival analysis of UK biobank data reveals associations between physical multimorbidity clusters and subsequent depression, has just been published in Nature Communications Medicine. The results have been highlighted by the MRC on the UKRI website and featured in its newsletter. See:
UKRI News: https://www.ukri.org/news/multiple-chronic-illnesses-linked-to-higher-risk-of-depression
Edinburgh University post: https://www.ed.ac.uk/news/multiple-chronic-illnesses-could-double-risk-of-depression
and
Full paper at: https://doi.org/10.1038/s43856-025-00825-7
Code at: https://github.com/laurendelong21/clusterMed
Scientific Reports Paper Out: Understanding hospital activity and outcomes for people with multimorbidity
Our paper come out in Nature Scientific Reports has just appeared. It investigates the relationships between in-hospital activity, multimorbidity and post-discharge outcomes in older adults. It’s available at: https://doi.org/10.1038/s41598-025-92940-7.
Our preprint on formally verified neurosymbolic trajectory learning is out on arXiv
Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces
Astract:
We present a novel formalisation of tensor semantics for linear temporal logic on finite traces (LTLf), with formal proofs of correctness carried out in the theorem prover Isabelle/HOL. We demonstrate that this formalisation can be integrated into a neurosymbolic learning process by defining and verifying a differentiable loss function for the LTLf constraints, and automatically generating an implementation that integrates with PyTorch. We show that, by using this loss, the process learns to satisfy pre-specified logical constraints. Our approach offers a fully rigorous framework for constrained training, eliminating many of the inherent risks of ad-hoc, manual implementations of logical aspects directly in an “unsafe” programming language such as Python, while retaining efficiency in implementation.
Our formalisation of Linear Resources and Process Compositions has been published in the Archive of Formal Proof
Abstract
In this entry we formalise a framework for process composition based on actions that are specified by their input and output resources. We verify their correctness by translating compositions of process into deductions of intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction.
We describe an earlier version of this formalisation in our article Linear Resources in Isabelle/HOL, which also includes a formalisation of manufacturing processes in the simulation game Factorio.
Jiawei Zheng passes his PhD Defence!
Congratulations to Jiawei Zheng who has passed his PhD viva with no corrections. His thesis on Process-aware Pattern Recognition and Deviation Detection Under Uncertainty was examined by Prof Juliana Bowles (St Andrews, external) and Prof David Robertson.
Our formalisation of Lie Groups and Algebras has been published in the Archive of Formal Proof
Abstract
Lie Groups are formalised as locales, building on the AFP theory of Smooth Manifolds. We formalise the diffeomorphism group of a manifold, and the action of a Lie group on a manifold. The general linear group is shown to be a Lie group by proving properties of the determinant, and matrix inverses. We also develop a theory of smooth vector fields on a manifold , defined as smooth maps from the manifold to its tangent bundle . We employ a shortcut that avoids difficulties in defining the tangent bundle as a manifold, but which still leads to vector fields with the properties one would expect. We then construct the Lie algebra of a Lie group as an algebra of left-invariant smooth vector fields.
Schmoetten R. and Fleuriot J. D. (2024). Lie Groups and Algebras. Archive of Formal Proofs. ISSN: 2150-914x.