.THY

L2Norm_Integral.thy (4.59 kB)

.THY

Minkowski_Integral_Inequality.thy (9.35 kB)

.THY

Small_Gain_Theorem.thy (42.84 kB)

1/0

# 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