2 papers
cs.LO2025
Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
Dustin Bryant, Jim Woodcock, Simon Foster
This paper presents a formalized analysis of the sigmoid function and a fully mechanized proof of the Universal Approximation Theorem (UAT) in Isabelle/HOL, a higher-order logic th…
cs.LO2024
Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
Simon Foster, Chung-Kil Hur, Jim Woodcock
Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the…