Компјутерски асистиран доказ

Од Википедија, слободната енциклопедија
Прејди на: содржини, барај

Компјутерски асистиран доказ е математички доказ кој е делумно генериран од компјутерот.

Повеќето компјутерски потпомогнати докази за датумот се имплементации на големи докази по исцрпување на математичка теорема. Идејата е за да се користи компјутерска програма која што ќе ги врши долгите пресметки, и со тоа обезбедува доказ дека резултатот од овие пресметки ја имплицира дадената теорема. Во 1976 година, четирибојната теорема беше првата голема теорема која беше потврдена со помош на компјутерска програма.

Направени се обиди во областа на вештачката интелегенција за да се создадат, нови, експлицитни и помали докази на математичките теореми. Како и автоматските докажувачи на теореми докажале поголем број на нови резултати и пронашле нови докази за познати теореми. Покрај тоа интерактивните докажувачки асистенти им овозможиле на математичарите да развијаат читливи докази кои се официјално потврдени за коректност. Иако овие докази може да се проверат од човек, тие не ги делат коннтраверзните импликации на компјутерски потпомогнатите докази.

Методи[уреди]

Еден метод се користи во докази поврзани со нумерички пресметки. Притоа се контролира грешката на заокружување и натрупувањето на грешките во интервалот на аритметичката техника. Поточно едно намалување на пресметките на секвенцата на основните оерации(+,-,*,/) резултира на елементарните операции кои се заокружени со компјутерска прецизност. Сепак, може да се конструираат интервали обезбедени од горните и долните граници на резултатите на елементарната операција. Потоа една придонесува со заменувањето на броевите со интервали и вршење на основните операции помеѓу истите.

Филозофски забелешки и приговори[уреди]

Компјутерските асистирани докази се предмет на многу контроверзи на математичкиот свет. Некои математичари сметаат дека долгите компјутерски асистирани докази не се, во извесна смисла, 'вистински' математички докази, бидејќи тие подразбираат многу логични чекори кои не се практични да се верификуваат од човечките битија и математичарите ефикасно се трудат да го заменат логичкото одбивање од претпоставената аксиома со доверба во емпириски пресметковен процес, кој е потенцијално погоден од грешките во компјутерската програма, како и дефекти во траењето во животната средина и хардверот. Другите математичари сметаат дека компјутерските асистирани докази треба да се сметаат како пресметки, наместо докази: алгоритамскиот доказ сам треба да се докаже валиден така што неговата употреба тогаш може да се смета како проверка. Ова е познато како 'принципот Поенкаре' во математичката заедница по изјавата на Henri Poincare. Аргументите за компјутерските асистирани докази се предмет на грешки во нивниот извор на програми, компајлери и хардвери. Друг можен начин на верификување на компјутерските асиститирани докази е да се гарантираат нивните расудувани чекори во машински читлива форма, а потоа се употребува автоматски провајдер за теореми за да ја покажат својата коректност. Овој пристап на користење на компјутерска програма за да се докаже друга програма, не е за да се задоволат скептиците на компјутерските докази кои тоа го гледаат како додавање на уште еден слој на сложеност без да се согледа потребата за човековите сфаќања. Друг аргумент против компјутерските асистирани докази е дека тие немаат математичка елеганција-кои ги обезбедуваат, немаат увид за нови корисни концепти. Дополнителни философски прашања од страна на компјутерските докази е дали тие се направи во математичка квази-емпириска наука, каде што на научниот метод станува поважен од примена на чист разум во областа на апстрактните математички концепти. Ова се однесува директно на аргументот во рамките на математиката за тоа дали математиката е врз основа на идеи, или "само" на една вежба во официјалниот симбол на манипулацијата. Таа исто така го покренува прашањето ако се насочите според гледањето на Платонистите, сите можни математички предмети во извесна смисла "веќе постојат", дали компјутерски-потпомогнатата математика е наука базирана на набљудување како астрономијата, повеќе отколку експериментална како физика или хемија. Интересно, во рамките на физичката заедница истовремено се поставува прашањето дали дваесет и првиот век теоретската физика треба да стане премногу математичка, и оставајќи ги зад себе своите експериментални корени.

Список на теореми докажани со помош на компјутерски програми[уреди]

Вклучувањето во овој список не повлекува дека постои формален доказ проверен со компјутер, туку повеќе дека компјутерска програма е употребена на некој начин. Видете ги главните статии за повеќе детали.

Додатна литература[уреди]

  • Lenat, D.B., (1976), AM: An artificial intelligence approach to discovery in mathematics as heuristic search, Ph.D. Thesis, STAN-CS-76-570, and Heuristic Programming Project Report HPP-76-8, Stanford University, AI Lab., Stanford, CA.

Надворешни линкови[уреди]