Skip to content

news

Our paper on differentiable Signal Temporal Logic for neurosymbolic AI has been published by LIPIcs

    GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning

    Authors Mark Chevallier , Filip Smola , Richard Schmoetten , Jacques D. Fleuriot 

    Part of: Volume: 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)
    Series: Leibniz International Proceedings in Informatics (LIPIcs)
    Conference: International Symposium on Temporal Representation and Reasoning (TIME)

    New pre-print out on our qualitative study of older adults living with sensors at home

      Our paper on “Early experiences and views of older adults living with sensing technology at home: A qualitative study” is available as a pre-print here.

      This study explored older adults’ perceptions and lived experiences of sensing technologies integrated into their home environments. Using semi-structured interviews and in-home observations, we examined how older individuals interacted with motion, magnetic, and physiological sensors embedded in their everyday routines.

      and it is a companion paper to our modelling paper currently available on arXiv as 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).

        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

          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.

            Paper: https://arxiv.org/abs/2501.13712

            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.