Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL. - Mark Chevallier; Jacques D. Fleuriot (CoRR, 2021)

Constrained Training of Neural Networks via Theorem Proving. - Mark Chevallier; Matthew Whyte; Jacques D. Fleuriot (OVERLAY@AI*IA, 2022)

Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces. - Mark Chevallier; Filip Smola; Richard Schmoetten; Jacques D. Fleuriot (CoRR, 2025)

GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning. - Mark Chevallier; Filip Smola; Richard Schmoetten; Jacques D. Fleuriot (CoRR, 2025)