3 files

Formal proof of the small-gain theorem by interactive theorem proving

posted on 2020-02-04, 12:01 authored by Omar Ahmad Jasim, Sandor Veres
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".





There is no personal data or any that requires ethical approval


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