How Deduction Systems Can Help You To Verify Stability Properties
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909543887273984 |
|---|---|
| author | Gleirscher, Mario Massoud, Rehab Hutter, Dieter Lüth, Christoph |
| author_facet | Gleirscher, Mario Massoud, Rehab Hutter, Dieter Lüth, Christoph |
| contents | Mathematical proofs are a cornerstone of control theory, and it is important to get them right. Deduction systems can help with this by mechanically checking the proofs. However, the structure and level of detail at which a proof is represented in a deduction system differ significantly from a proof read and written by mathematicians and engineers, hampering understanding and adoption of these systems.
This paper aims at helping to bridge the gap between machine-checked proofs and proofs in engineering and mathematics by presenting a machine-checked proof for stability using Lyapunov's theorem in a human-readable way. The structure of the proof is analyzed in detail, and potential benefits of such a proof are discussed, such as generalizability, reusability and increased trust in correctness. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_10747 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | How Deduction Systems Can Help You To Verify Stability Properties Gleirscher, Mario Massoud, Rehab Hutter, Dieter Lüth, Christoph Systems and Control Mathematical proofs are a cornerstone of control theory, and it is important to get them right. Deduction systems can help with this by mechanically checking the proofs. However, the structure and level of detail at which a proof is represented in a deduction system differ significantly from a proof read and written by mathematicians and engineers, hampering understanding and adoption of these systems. This paper aims at helping to bridge the gap between machine-checked proofs and proofs in engineering and mathematics by presenting a machine-checked proof for stability using Lyapunov's theorem in a human-readable way. The structure of the proof is analyzed in detail, and potential benefits of such a proof are discussed, such as generalizability, reusability and increased trust in correctness. |
| title | How Deduction Systems Can Help You To Verify Stability Properties |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2404.10747 |