Formally Verified Neurosymbolic Trajectory Learning via Tensor-based
Linear Temporal Logic on Finite Traces
Formally Verified Neurosymbolic Trajectory Learning via Tensor-based
Linear Temporal Logic on Finite Traces
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 …