The University of Sheffield
Browse
.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
3 files

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

Download all (56.77 kB)
software
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".

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

Usage metrics

    Department of Automatic Control and Systems Engineering

    Categories

    Keywords

    Isabelle/HOLformal verificationcontrol theoryControl Systems, Robotics and AutomationAutomation and Control Engineering

    Licence

    GPL 2.0+

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC