Schutz' Independent Axioms for Minkowski Spacetime. - Richard Schmoetten; Jake E. Palmer; Jacques D. Fleuriot (Arch. Formal Proofs, 2021)

Formalising Geometric Axioms for Minkowski Spacetime and Without-Loss-of-Generality Theorems. - Richard Schmoetten; Jake E. Palmer; Jacques D. Fleuriot (ADG, 2021)

Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. - Richard Schmoetten; Jake E. Palmer; Jacques D. Fleuriot (J. Autom. Reason., 2022)

Correction: Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. - Richard Schmoetten; Jake E. Palmer; Jacques D. Fleuriot (J. Autom. Reason., 2023)

Lie Groups and Algebras. - Richard Schmoetten; Jacques D. Fleuriot (Arch. Formal Proofs, 2024)

A Construction of the Lie Algebra of a Lie Group in Isabelle/HOL. - Richard Schmoetten; Jacques D. Fleuriot (CoRR, 2024)

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)

Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL. - Richard Schmoetten; Jacques D. Fleuriot (J. Autom. Reason., 2025)