A Caltech Library Service

Complexity in Automation of SOS Proofs: An Illustrative Example

Gayme, Dennice and Fazel, Maryam and Doyle, John C. (2006) Complexity in Automation of SOS Proofs: An Illustrative Example. In: Proceedings of the 45th IEEE Conference on Decision and Control. IEEE Conference on Decision and Control. IEEE , Piscataway, N.J., pp. 5851-5856. ISBN 978-1-4244-0170-3.

PDF - Published Version
See Usage Policy.


Use this Persistent URL to link to this item:


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.’

Item Type:Book Section
Related URLs:
Gayme, Dennice0000-0003-0330-415X
Doyle, John C.0000-0002-1828-2486
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.
Other Numbering System:
Other Numbering System NameOther Numbering System ID
INSPEC Accession Number9430669
Series Name:IEEE Conference on Decision and Control
Record Number:CaltechAUTHORS:20110215-132231555
Persistent URL:
Official Citation:Gayme, D.; Fazel, M.; Doyle, J.C.; , "Complexity in Automation of SOS Proofs: An Illustrative Example," Decision and Control, 2006 45th IEEE Conference on , vol., no., pp.5851-5856, 13-15 Dec. 2006 doi: 10.1109/CDC.2006.377629 URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:22222
Deposited By: Benjamin Perez
Deposited On:15 Feb 2011 21:59
Last Modified:09 Nov 2021 16:03

Repository Staff Only: item control page