CaltechAUTHORS
Published 2006 | Version Published
Book Section - Chapter Open

Complexity in Automation of SOS Proofs: An Illustrative Example

Creators

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

Gayme2006p9089Proceedings_Of_The_46Th_Ieee_Conference_On_Decision_And_Control_Vols_1-14.pdf

Files (1.9 MB)

Additional details

Identifiers

Eprint ID
22222
Resolver ID
CaltechAUTHORS:20110215-132231555

Dates

Created
2011-02-15
Created from EPrint's datestamp field
Updated
2021-11-09
Created from EPrint's last_modified field

Caltech Custom Metadata

Series Name
IEEE Conference on Decision and Control
Other Numbering System Name
INSPEC Accession Number
Other Numbering System Identifier
9430669