1 citations · 1 across the 3 of their papers we have counts for
Showing cs.AIShow all
2 papers · 1 filter
cs.AI2025
Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces
Mark Chevallier, Filip Smola, Richard Schmoetten +1
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…
cs.AI2022★ 1 cited
Constrained Training of Neural Networks via Theorem Proving
Mark Chevallier, Matthew Whyte, Jacques D. Fleuriot
We introduce a theorem proving approach to the specification and generation of temporal logical constraints for training neural networks. We formalise a deep embedding of linear te…