10.15131/shef.data.11791449
Omar Ahmad Jasim
Sandor Veres
Formal proof of the small-gain theorem by interactive theorem proving
2020
The University of Sheffield
Isabelle/HOL
formal verification
control theory
2020-02-04 12:01:51
article
https://figshare.shef.ac.uk/articles/software/Formal_proof_of_the_small-gain_theorem_by_interactive_theorem_proving/11791449
<div>This is source code of the formal proof of the Small-gain theorem in Isabelle/HOL theorem prover. This code is part of the paper "Towards Formal Proofs of Feedback Control Theory" presented in System Theory, Control and Computing (ICSTCC) conference published in IEEE - DOI: 10.1109/ICSTCC.2017.8107009 <br></div><div><br></div><div>Note: Put both files "L2Norm_Integral.thy" and
"Minkowski_Integral_Inequality.thy" in the main Isabelle's directory
before loading the main theorem file "Small_Gain_Theorem.thy".</div>