Formal proof of the small-gain theorem by interactive theorem proving
softwareposted on 04.02.2020 by Omar Ahmad Jasim, Sandor Veres
Code as a research output can either be uploaded directly from your computer or through the code management system GitHub. Versioning of code repositories is supported.
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
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".
EthicsThere is no human data or any that requires ethical approval
PolicyThe data complies with the funder's policy on access and sharing
Sharing and access restrictionsThe data can be shared openly
- The file formats are open or commonly used
Methodology, headings and units
- Headings and units are explained in the files