Jasim, Omar Ahmad
Veres, Sandor
Formal proof of the small-gain theorem by interactive theorem proving
<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>
Isabelle/HOL;formal verification;control theory
2020-02-04
https://figshare.shef.ac.uk/articles/software/Formal_proof_of_the_small-gain_theorem_by_interactive_theorem_proving/11791449

10.15131/shef.data.11791449