(Downloads - 0)
For more info about our services contact : help@bestpfe.com
Table of contents
1 Introduction
1.1 Problems Involving Computer Assisted Proofs
1.1.1 Nonlinear Inequalities arising in the Flyspeck Project
1.1.2 Formal Global Optimization Problems
1.1.3 Non Commutative Optimization
1.2 Certified Global Optimization in the Literature
1.3 Contribution
1.3.1 A General Certification Scheme
1.3.2 Software Implementation in OCAML and COQ
1.4 Outline
I A General Framework for Certified Global Optimization
2 Sums of Squares based Optimization
2.1 SDP and Interior-Points methods
2.2 Application of SDP to Polynomial Optimization
2.3 Application of SDP to Semialgebraic Optimization
2.4 Exploiting the System Properties
2.5 Hybrid Symbolic-Numeric Certification
3 A General Approximation Scheme
3.1 Abstract Syntax Tree of Multivariate Transcendental Functions
3.2 Combining Semialgebraic Approximations and SOS
3.3 Convergence of the Approximation Algorithm
II Nonlinear Optimization via Maxplus Templates
4 Minimax Semialgebraic Optimization
4.1 Minimax Univariate Polynomials
4.2 Combining Minimax Approximations and SOS
4.3 Numerical Test Results
4.4 Convergence Properties
4.5 Taylor Expansions
5 Maxplus Semialgebraic Estimators and SOS
5.1 The Basis of Maxplus Functions
5.2 Maxplus Approximation for Semiconvex Functions
5.3 Combining Maxplus Approximations and SOS
5.3.1 An Adaptive Semialgebraic Approximation Algorithm
5.3.2 An Optimization Algorithm based on Maxplus Estimators
5.3.3 Convergence Results
5.3.4 Refining Bounds by Domain Subdivisions
5.4 Numerical Results
5.4.1 Flyspeck Inequalities
5.4.2 Random Inequalities
5.4.3 Certification of MetiTarski Bounds
6 The Templates Method
6.1 Max-plus Approximations and Nonlinear Templates
6.2 Reducing the Size of SOS Relaxations for POP
6.2.1 Lower Bounds of Interval Matrix Minimal Eigenvalues
6.2.2 A Template Algorithm for POP
6.2.3 Numerical Results
6.3 Underestimators for Semialgebraic Functions
6.3.1 Best Polynomial Underestimators
6.3.2 A Convergent Hierarchy of Semidefinite Relaxations
6.3.3 Exploiting Sparsity
6.3.4 Numerical Experiments
6.4 The Template Optimization Algorithm
6.5 Benchmarks
6.5.1 Comparing three certification methods
6.5.2 Global optimization problems
6.5.3 Certification of various Flyspeck inequalities
III From Certified to Formal Global Optimization
7 Formal Nonlinear Global Optimization
7.1 The COQ Proof Assistant
7.1.1 A Formal Theorem Prover
7.1.2 Logic and Computation
7.1.3 Computational Reflection
7.2 Polynomial Arithmetic in COQ
7.2.1 From Binary Integers to Arbitrary-size Rationals
7.2.2 The polynomial ring structure
7.3 Formal Polynomial Optimization
7.3.1 Encoding Putinar Certificates
7.3.2 Bounding the Polynomial Remainder
7.3.3 Checking Polynomial Equalities
7.3.4 Checking Polynomial Nonnegativity
7.4 Beyond Polynomial Inequalities
7.4.1 Intervals
7.4.2 Semialgebraic expressions
7.4.3 POP relaxations
7.4.4 Formal Bounds for Semialgebraic Functions
8 Conclusion and Perspectives
8.1 Achievements
8.2 Perspectives
8.2.1 Complexity of the nonlinear template method
8.2.2 Extension to global optimization with transcendental constraints
8.2.3 Extension to nonlinear optimal control problems
8.2.4 Formal procedures for nonlinear reasoning
A Flyspeck Nonlinear Inequalities
A.1 Semialgebraic Flyspeck Inequalities
A.2 Transcendental Flyspeck Inequalities
A.2.1 Small-sized Flyspeck Inequalities
A.2.2 Medium-size Flyspeck Inequalities
B The NLCertify Package
B.1 Source Code Organization
B.2 Installation of the NLCertify Package
B.2.1 Compilation Dependencies
B.2.2 Installation
B.3 User Parameters
B.3.1 General Parameters
B.3.2 POP/SDP Relaxations Parameters
B.4 Certification of Nonlinear Inequalities
B.4.1 Input Settings
B.4.2 NLCertify Execution
