Complexity in Automation of SOS Proofs: An Illustrative Example
- Creators
-
Gayme, Dennice
- Fazel, Maryam
-
Doyle, John C.
Abstract
We present a case study in proving invariance for a chaotic dynamical system, the logistic map, based on Positivstellensatz refutations, with the aim of studying the problems associated with developing a completely automated proof system. We derive the refutation using two different forms of the Positivstellensatz and compare the results to illustrate the challenges in defining and classifying the 'complexity' of such a proof. The results show the flexibility of the SOS framework in converting a dynamics problem into a semialgebraic one as well as in choosing the form of the proof. Yet it is this very flexibility that complicates the process of automating the proof system and classifying proof 'complexity.'
Additional Information
© 2006 IEEE. Issue Date: 13-15 Dec. 2006, Date of Current Version: 07 May 2007. The authors would like to thank Stephen Prajna for his great patience, many helpful suggestions and discussions.Attached Files
Published - Gayme2006p9089Proceedings_Of_The_46Th_Ieee_Conference_On_Decision_And_Control_Vols_1-14.pdf
Files
| Name | Size | Download all |
|---|---|---|
|
md5:1eb60879a90a9c6fae25b045dc5fcfad
|
1.9 MB | Preview Download |
Additional details
- Eprint ID
- 22222
- Resolver ID
- CaltechAUTHORS:20110215-132231555
- Created
-
2011-02-15Created from EPrint's datestamp field
- Updated
-
2021-11-09Created from EPrint's last_modified field
- Series Name
- IEEE Conference on Decision and Control
- Other Numbering System Name
- INSPEC Accession Number
- Other Numbering System Identifier
- 9430669