Complexity in Automation of SOS Proofs: An Illustrative Example

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.