Computing Certificates of Members in Archimedean Quadratic Modules in \(\mathbb{A}[X]\) and Certifying the Emptiness in Inconsistent Monogenic Archimedean Quadratic Modules in \(\mathbb{A}[X_1, \dots, X_n]\)
Date:
Polynomials have been found to be a powerful tool over hundreds of years for modeling problems in numerous applications in science, engineering, medicine, and other domains; convex optimization, as an example, has many applications. In the context of formal methods, polynomials arise in modeling in aerospace software and robotics–especially collision avoidance, cyber-physical and hybrid systems, autonomous vehicles and controllers based on neural networks. Optimization of a polynomial function subject to polynomial constraints is investigated in many areas–to mention a few, scheduling, resource allocation, financial systems including option pricing and portfolio optimization, quantum information systems, control and system theory, particularly analysis of dynamical systems such as stability, equilibrium, and more recently, in sophisticated modeling of neurons in deep neural networks and machine learning. Modern SMT solvers and theorem provers often resort to linear approximations of polynomials as a pragmatic solution due to the inherent complexities associated with reasoning about polynomial inequalities.
A quadratic module is a linear combination of polynomials in a set of generators (augmented with the constant 1) with sum of squares polynomials as multipliers. This is in contrast to an ideal being the set of polynomials as a linear combination of generators in which multipliers are simply polynomials. The membership problem for a finitely generated quadratic module can be decided; however, computing a certificate exhibiting why it is nonnegative under the assumption that the generators are nonnegative, can be nontrivial.
This thesis proposes a new symbolic algorithm to compute a certificate for members in Archimedean quadratic modules in the general univariate case, i.e., no constraints are imposed on the set of generators nor the input polynomial. The algorithm takes as input a set of generators \(G\) and an input polynomial \(f \in QM(G)\). The certificate witnessing the membership of \(f\) in the quadratic module generated by \(G\) uses the original set of generators \(G\).
Finally, an algorithm to compute a certificate for \(-1\) in inconsistent quadratic modules in \(\mathbb{A}[X_1, \dots, X_n]\) is presented. The algorithm has two parts. The first part computes an upperbound of \(g\) to obtain a B'ezout-like identity for \(-1\). The second part lifts nonnegative polynomials to become sums of squares adding additional terms in the monogenic quadratic module.