Abstrakt. Vi presenterar ett formellt verktyg för att verifiera multivariata icke-linjära ojämlikheter. Vår verifieringsmetod är baserad på intervall aritmetik med Taylor approximationer. Vårt verktyg är implementerat i HOL Light proof assistent och det är kapabelt att verifiera multivariat icke-linjär polynom och icke-polynomiska ojämlikheter på rektangulära domäner. Ett av huvuddragen i vårt arbete är ett effektivt genomförande av verifieringsförfarandet som kan bevisa icke-trivial högdimensionell ojämlikhet på flera sekunder. Vi utvecklade verifieringsverktyget som en del av Flyspeck-projektet (ett formellt bevis på Keplers gissning). Flyspeck-projektet omfattar cirka 1000 icke-linjära ojämlikheter. Vi testade framgångsrikt vår metod på mer än 100 Flyspeck ojämlikheter och uppskattade att det formella verifieringsförfarandet är ca 3000 gånger långsammare än en informell verifieringsmetod som genomförs i C++. Vi beskriver även framtida arbete och framtida optimeringar för vår metod.
Ett annat beslutsförfarande för HOL Light proof assistent har tagits fram som en del av Flyspeck projekt 1: verifiera_ineq REF.
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations
{'venue': 'ArXiv', 'journal': 'ArXiv', 'mag_field_of_study': ['Computer Science', 'Mathematics']}