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 approvalPolicy
The data complies with the institution and funders' policies on access and sharingSharing and access restrictions
The data can be shared openlyData description
- The file formats are open or commonly used
Methodology, headings and units
- Headings and units are explained in the files
