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)
Abstract:
We present GradSTL, the first fully comprehensive implementation of signal temporal logic (STL) suitable for integration with neurosymbolic learning. In particular, GradSTL can successfully evaluate any STL constraint over any signal, regardless of how it is sampled. Our formally verified approach specifies smooth STL semantics over tensors, with formal proofs of soundness and of correctness of its derivative function. Our implementation is generated automatically from this formalisation, without manual coding, guaranteeing correctness by construction. We show via a case study that using our implementation, a neurosymbolic process learns to satisfy a pre-specified STL constraint. Our approach offers a highly rigorous foundation for integrating signal temporal logic and learning by gradient descent.
Paper: https://www.arxiv.org/abs/2508.04438
This work has been accepted as a long paper at TIME 2025 and will be presented at the conference at the end of August 2025.
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.
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.