Formal proof of the small-gain theorem by interactive theorem proving
software
posted on 2020-02-04, 12:01 authored by Omar Ahmad Jasim, Sandor VeresThis 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".
Funding
EP/L024942/1
History
Ethics
- There is no personal data or any that requires ethical approval
Policy
- The data complies with the institution and funders' policies on access and sharing
Sharing and access restrictions
- The data can be shared openly
Data description
- The file formats are open or commonly used
Methodology, headings and units
- Headings and units are explained in the files
