- TITLE: Complexity in Automation of SOS Proofs: An Illustrative Example
- AUTHORS: Dennice Gayme, Maryam Fazel, John Doyle, .
- 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.'
- STATUS: Proc. of Conference on Decision and Control, Dec 2006.
- paper: pdf file