Аутоматско доказивање теорема

Аутоматско доказивање теорема (такође познато као аутоматизована дедукција) је подобласт аутоматског закључивања и математичке логике која се бави доказивањем математичких теорема помоћу компјутерских програма. Аутоматско резоновање о математичком доказу било је главни подстицај за развој рачунарске науке.

Логичке основе

Док корени формализоване логике сежу до Аристотела, крајем 19. и почетком 20. века дошло је до развоја модерне логике и формализоване математике. Фрегеов Бегриффссцхрифт (1879) увео је и потпуни пропозициони рачун и оно што је у суштини модерна предикатска логика.^[1] Његове Основе аритметике, објављене 1884. године,^[2] су изразиле (делове) математике у формалној логици. Овај приступ су наставили Расел и Вајхед у својој утицајној Принципиа Матхематица, која је први пут објављена 1910–1913,^[3] и са ревидираним другим издањем 1927.^[4] Расел и Вајтхед су сматрали да могу да формализују сву математичку истину користећи аксиоме и правила закључивања формалне логике, у принципу отварајући процес аутоматизацији. Године 1920, Торалф Сколем је поједноставио претходни резултат Леополда Ловенхајма, што је довело до Ловенхајм–Сколемове теореме, а 1930. до појма Хербрандовог универзума и Хербрандове интерпретације која је дозвољавала (не)задовољивост формула првог реда (и стога ваљаност теореме) да се сведе на (потенцијално бесконачно много) проблема пропозиционе задовољивости.^[5]

Године 1929, Мојжеш Пресбургер је показао да је теорија првог реда природних бројева са сабирањем и једнакошћу (сада у његову част названа Пресбургерова аритметика) одлучива и дао је алгоритам који може да утврди да ли је дата реченица у језику тачна или нетачна.^[6]^[7]

Међутим, убрзо након овог позитивног резултата, Курт Гедел је објавио дело О формално неодлучивим пропозицијама Принципиа Матхематица и сродним системима (1931), показујући да у сваком довољно снажном аксиоматском систему постоје истините тврдње које се у систему не могу доказати. Ову тему су тридесетих година прошлог века даље развили Алонзо Черч и Алан Тјуринг, који су с једне стране дали две независне, али еквивалентне дефиниције израчунљивости, а са друге конкретне примере неодлучивих питања.

Референце

^ Фреге, Готтлоб (1879). Бегриффссцхрифт. Верлаг Лоуис Неуерт.
^ Фреге, Готтлоб (1884). Дие Грундлаген дер Аритхметик (ПДФ). Бреслау: Wилхелм Кобнер. Архивирано из оригинала (ПДФ) 2007-09-26. г. Приступљено 2012-09-02.
^ Русселл, Бертранд; Wхитехеад, Алфред Нортх (1910—1913). Принципиа Матхематица (1ст изд.). Цамбридге Университy Пресс.
^ Русселл, Бертранд; Wхитехеад, Алфред Нортх (1927). Принципиа Матхематица (на језику: енглески) (2нд изд.). Цамбридге Университy Пресс.
^ Хербранд, Ј. (1930). Рецхерцхес сур ла тхéорие де ла дéмонстратион (ПхД) (на језику: француски). Университy оф Парис.
^ Пресбургер, Мојżесз (1929). „Üбер дие Воллстäндигкеит еинес геwиссен Сyстемс дер Аритхметик ганзер Захлен, ин wелцхем дие Аддитион алс еинзиге Оператион хервортритт”. Цомптес Рендус ду I Цонгрèс де Матхéматициенс дес Паyс Славес. Wарсзаwа: 92—101.
^ Давис, Мартин (2001). „Тхе Еарлy Хисторy оф Аутоматед Дедуцтион”. Робинсон & Воронков 2001. Архивирано из оригинала 2012-07-28. г. Приступљено 2012-09-08.

Литература

Цханг, Цхин-Лианг; Лее, Рицхард Цхар-Тунг (2014) [1973]. Сyмболиц Логиц анд Мецханицал Тхеорем Провинг. Елсевиер. ИСБН 9780080917283.
Ловеланд, Доналд W. (2016) [1978]. Аутоматед Тхеорем Провинг: А Логицал Басис. Фундаментал Студиес ин Цомпутер Сциенце. 6. Елсевиер. ИСБН 9781483296777.
Луцкхам, Давид (1990). Программинг wитх Специфицатионс: Ан Интродуцтион то Анна, А Лангуаге фор Специфyинг Ада Програмс. Спрингер. ИСБН 978-1461396871.
Галлиер, Јеан Х. (2015) [1986]. Логиц фор Цомпутер Сциенце: Фоундатионс оф Аутоматиц Тхеорем Провинг (2нд изд.). Довер. ИСБН 978-0-486-78082-5. „Тхис материал маy бе репродуцед фор анy едуцатионал пурпосе, ...”
Дуффy, Давид А. (1991). Принциплес оф Аутоматед Тхеорем Провинг. Wилеy. ИСБН 9780471927846.
Wос, Ларрy; Овербеек, Росс; Луск, Еwинг; Боyле, Јим (1992). Аутоматед Реасонинг: Интродуцтион анд Апплицатионс (2нд изд.). МцГраw–Хилл. ИСБН 9780079112514.
Робинсон, Алан; Воронков, Андреи, ур. (2001). Хандбоок оф Аутоматед Реасонинг. I. Елсевиер, МИТ Пресс. ИСБН 9780080532790. II ISBN 9780262182232.
Фиттинг, Мелвин (2012) [1996]. Фирст-Ордер Логиц анд Аутоматед Тхеорем Провинг (2нд изд.). Спрингер. ИСБН 9781461223603.

Спољашње везе

А лист оф тхеорем провинг тоолс

[1] Фреге, Готтлоб (1879). Бегриффссцхрифт. Верлаг Лоуис Неуерт.

[2] Фреге, Готтлоб (1884). Дие Грундлаген дер Аритхметик (ПДФ). Бреслау: Wилхелм Кобнер. Архивирано из оригинала (ПДФ) 2007-09-26. г. Приступљено 2012-09-02.

[3] Русселл, Бертранд; Wхитехеад, Алфред Нортх (1910—1913). Принципиа Матхематица (1ст изд.). Цамбридге Университy Пресс.

[4] Русселл, Бертранд; Wхитехеад, Алфред Нортх (1927). Принципиа Матхематица (на језику: енглески) (2нд изд.). Цамбридге Университy Пресс.

[5] Хербранд, Ј. (1930). Рецхерцхес сур ла тхéорие де ла дéмонстратион (ПхД) (на језику: француски). Университy оф Парис.

[6] Пресбургер, Мојżесз (1929). „Üбер дие Воллстäндигкеит еинес геwиссен Сyстемс дер Аритхметик ганзер Захлен, ин wелцхем дие Аддитион алс еинзиге Оператион хервортритт”. Цомптес Рендус ду I Цонгрèс де Матхéматициенс дес Паyс Славес. Wарсзаwа: 92—101.

[Davis2001-7] Давис, Мартин (2001). „Тхе Еарлy Хисторy оф Аутоматед Дедуцтион”. Робинсон & Воронков 2001. Архивирано из оригинала 2012-07-28. г. Приступљено 2012-09-08.

[1]

[2]

[3]

[4]

[5]

[6]

[7]