Доказові обчислення — цілеспрямовані комп'ютерні обчислення, комбіновані з аналітичними дослідженнями, які призводять до строгого встановлення нових фактів і доведення теорем.
Достовірні обчислення
Одним із часто застосовуваних методів доказових обчислень є достовірні обчислення. Під достовірними обчисленнями мають на увазі чисельні методи з автоматичною верифікацією точності одержуваних результатів. Досить часто доказові обчислення будуються на основі інтервального аналізу, де замість дійсних чисел розглядаються інтервали, які визначають точність величин. Інтервальний аналіз широко застосовується для обчислень з гарантованою точністю в умовах машинної арифметики.
Приклади
У теорії чисел
Завдяки тому, що теорія чисел багато в чому оперує цілими числами, використання доказових обчислень у теорії чисел виявляється дуже плідним.
- Стверджується, що число Мерсенна є простим. Перевірити цей факт теоретично може людина, але практично — лише з використанням обчислювальної техніки.
- Л. Ейлер висунув гіпотезу, що рівняння не має розв'язків у цілих додатних числах. Проте пізніше було показано, що існує принаймні один розв'язок:
- , , , , .
Причому цей розв'язок знайдено шляхом перебору на комп'ютері.
У теорії графів
Одним з найвідоміших успішних застосувань доказових обчислень у теорії графів є розв'язання проблеми чотирьох фарб. Цю відому задачу поставлено 1852 року і сформульовано так: «з'ясувати, чи можна кожну розташовану на сфері карту розфарбувати чотирма фарбами так, щоб будь-які дві ділянки, які мають спільну межу, були розфарбовані в різні кольори». 1976 року [en] і [en] за допомогою доказових обчислень показали, що так можна розфарбувати будь-яку карту.
У гідродинаміці
Застосуванням доказових обчислень у математичних задачах гідродинаміки систематично займалися в під керівництвом [ru]. Прикладом є така теорема, отримана з допомогою доказових обчислень:
Теорема. При і спектральна має власне значення, яке лежить у півплощині . Отже, в лінеаризованій постановці за цих параметрів течія Пуазейля нестійка.
Ще приклади
- Проблема трійок Буля — Піфагора.
- Класифікація багатогранників Джонсона.
Див. також
Примітки
- Бабенко К. И. . Основы численного анализа. — М. : Наука, 1986.
- Кулиш У., Рац Д., Хаммер Р., Хокс М. Достоверные вычисления. Базовые численные методы. — РХД, 2005.
- Бабенко К. И., Васильев М. М. О доказательных вычислениях в задаче об устойчивости течения Пуазейля // ДАН СССР. — 1983. — Т. 273, № 6 (16 червня). — С. 1289—1294.
Література
- Панков П.С. Доказательные вычислениях на электронно-вычислительных машинах. — Фрунзе : Илим, 1978. — 179 с.
- К. И. Бабенко. О доказательных вычислениях и математическом эксперименте на ЭВМ // УМН. — 1985. — Т. 40, № 4(244) (16 червня). — С. 137—138.
- Бабенко К. И., Петрович В. Ю., Рахманов А. И. О доказательном эксперименте в теории поверхностных волн конечной амплитуды // Докл. АН. . — 1988. — Т. 303, № 5 (16 червня). — С. 1033—1037.
Посилання
- Інтервальний аналіз та його застосування [ 31 жовтня 2020 у Wayback Machine.]
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Dokazovi obchislennya cilespryamovani komp yuterni obchislennya kombinovani z analitichnimi doslidzhennyami yaki prizvodyat do strogogo vstanovlennya novih faktiv i dovedennya teorem Dostovirni obchislennyaOdnim iz chasto zastosovuvanih metodiv dokazovih obchislen ye dostovirni obchislennya Pid dostovirnimi obchislennyami mayut na uvazi chiselni metodi z avtomatichnoyu verifikaciyeyu tochnosti oderzhuvanih rezultativ Dosit chasto dokazovi obchislennya buduyutsya na osnovi intervalnogo analizu de zamist dijsnih chisel rozglyadayutsya intervali yaki viznachayut tochnist velichin Intervalnij analiz shiroko zastosovuyetsya dlya obchislen z garantovanoyu tochnistyu v umovah mashinnoyi arifmetiki PrikladiU teoriyi chisel Zavdyaki tomu sho teoriya chisel bagato v chomu operuye cilimi chislami vikoristannya dokazovih obchislen u teoriyi chisel viyavlyayetsya duzhe plidnim Stverdzhuyetsya sho chislo Mersenna M43112609 243112609 1 displaystyle M 43112609 2 43112609 1 ye prostim Pereviriti cej fakt teoretichno mozhe lyudina ale praktichno lishe z vikoristannyam obchislyuvalnoyi tehniki L Ejler visunuv gipotezu sho rivnyannya x15 x25 x35 x45 x55 displaystyle x 1 5 x 2 5 x 3 5 x 4 5 x 5 5 ne maye rozv yazkiv u cilih dodatnih chislah Prote piznishe bulo pokazano sho isnuye prinajmni odin rozv yazok x1 27 displaystyle x 1 27 x2 84 displaystyle x 2 84 x3 110 displaystyle x 3 110 x4 133 displaystyle x 4 133 x5 144 displaystyle x 5 144 Prichomu cej rozv yazok znajdeno shlyahom pereboru na komp yuteri U teoriyi grafiv Odnim z najvidomishih uspishnih zastosuvan dokazovih obchislen u teoriyi grafiv ye rozv yazannya problemi chotiroh farb Cyu vidomu zadachu postavleno 1852 roku i sformulovano tak z yasuvati chi mozhna kozhnu roztashovanu na sferi kartu rozfarbuvati chotirma farbami tak shob bud yaki dvi dilyanki yaki mayut spilnu mezhu buli rozfarbovani v rizni kolori 1976 roku en i en za dopomogoyu dokazovih obchislen pokazali sho tak mozhna rozfarbuvati bud yaku kartu U gidrodinamici Zastosuvannyam dokazovih obchislen u matematichnih zadachah gidrodinamiki sistematichno zajmalisya v pid kerivnictvom ru Prikladom ye taka teorema otrimana z dopomogoyu dokazovih obchislen Teorema Pri a 1 02 displaystyle alpha 1 02 i R 6000 displaystyle R 6000 spektralna maye vlasne znachennya yake lezhit u pivploshini Rel gt 0 displaystyle mathrm Re lambda gt 0 Otzhe v linearizovanij postanovci za cih parametriv techiya Puazejlya nestijka She prikladi Problema trijok Bulya Pifagora Klasifikaciya bagatogrannikiv Dzhonsona Div takozhDovedennya Eksperimentalna matematikaPrimitkiBabenko K I Osnovy chislennogo analiza M Nauka 1986 Kulish U Rac D Hammer R Hoks M Dostovernye vychisleniya Bazovye chislennye metody RHD 2005 Babenko K I Vasilev M M O dokazatelnyh vychisleniyah v zadache ob ustojchivosti techeniya Puazejlya DAN SSSR 1983 T 273 6 16 chervnya S 1289 1294 LiteraturaPankov P S Dokazatelnye vychisleniyah na elektronno vychislitelnyh mashinah Frunze Ilim 1978 179 s K I Babenko O dokazatelnyh vychisleniyah i matematicheskom eksperimente na EVM UMN 1985 T 40 4 244 16 chervnya S 137 138 Babenko K I Petrovich V Yu Rahmanov A I O dokazatelnom eksperimente v teorii poverhnostnyh voln konechnoj amplitudy Dokl AN 1988 T 303 5 16 chervnya S 1033 1037 PosilannyaIntervalnij analiz ta jogo zastosuvannya 31 zhovtnya 2020 u Wayback Machine