Cover Люксембург А.А. Автоматизированное построение математических теорий
Id: 27096
6.9 EUR

Автоматизированное построение математических теорий

URSS. 32 pp. (Russian). ISBN 5-354-01005-5. Second-hand. Condition: 4+.
  • Paperback
Серия: Relata Refero

Summary

Изучается возможность автоматизированного построения математических теорий. Рассматривается дедуктивная система, основанная на языке логики предикатов первого порядка, объектами системы являются математические выражения или формулы, которые описывают математические объекты или их свойства. В дедуктивной системе выводятся математические определения и теоремы. Для доказательства теорем используются методы автоматического доказательства. Разработан ...(More)алгоритм, выводящий часть формул системы. Для решения задачи используется аппарат математической логики, искусственного интеллекта, теории дедуктивных систем и теории семантических сетей.

Для студентов, аспирантов, математиков.


Soderzhanie
Vvedenie
 1.Opisanie deduktivnoj sistemi
 2.Predstavlenie dannikh v vide semanticheskoj seti
 3.Sravnenie opisannoj deduktivnoj sistemi s drugimi
 4.Algoritm vivoda, analiza i perevoda na estestvennij yazik matematicheskikh virazhenij
  4.1.Spisok funktsij (blokov) programmi
  4.2.Opisanie blokov algoritma
 5.Vzaimodejstvie programmi s ekspertom
 6.Rezul'tati raboti programmi
 7.Deduktsiya i poznanie
  7.1.Apriornost' kategorij i logiki
  7.2.Apriornost' iskhodnikh predstavlenij matematiki
  7.3.Real'nost' matematicheskikh ob'ektov
Spisok literaturi

Vvedenie

Sozdanie matematicheskoj teorii yavlyaetsya yarkim primerom intellektual'noj deyatel'nosti lyudej i tvorcheskogo protsessa. Zadacha formalizatsii vivoda matematicheskoj teorii otnositsya k zadacham iskusstvennogo intellekta. V knige rassmatrivaetsya deduktivnaya sistema vivoda formul formal'nogo yazika, vklyuchayuschego v sebya matematicheskie utverzhdeniya i opredeleniya matematicheskikh ob'ektov.

Istoricheski matematika formirovalas' iz nuzhd prakticheskoj deyatel'nosti lyudej, mnogie matematicheskie ponyatiya i teorii bili abstraktnim ili idealizirovannim otrazheniem dejstvitel'nosti, okruzhayuschego mira, t.e. nosili empiricheskij kharakter. Zatem s razvitiem matematicheskoj logiki, matematika stanovilas' vse bolee formalizovannoj naukoj. Posle poyavleniya komp'yuterov mnogie matematicheskie zadachi stalo vozmozhnim reshat' s ikh pomosch'yu.

V matematike est' ponyatiya i sootvetstvuyuschie teorii: ravenstvo, funktsiya, element, mnozhestvo, otnoshenie, graf, vklyuchenie, peresechenie, ob'edinenie, dopolnenie, raznost', operatsiya, svojstvo, mera, metrika, integral, predel, proizvodnaya, natural'nie chisla, kompleksnie chisla, dejstvitel'nie chisla, algebraicheskie strukturi: gruppi, kol'tsa, polya; okrestnost', neprerivnost', razmernost', kompaktnost', geometricheskie figuri, mnogoobraziya, topologicheskie strukturi i t.d. i t.p.

V printsipe vse visheizlozhennie ponyatiya i teorii, ikh kasayuschiesya, mogut bit' sformulirovani dostatochno formal'no. Tochnogo matematicheskogo opredeleniya, chto takoe matematicheskaya teoriya -- net. Mozhno govorit', chto matematicheskaya teoriya -- eto nabor formul, ili nabor aksiom i formul, kotorie mogut bit' vivedeni iz aksiom. No takie opredeleniya ne otrazhayut soderzhatel'noj storoni teorii. Chtobi tochnee okharakterizovat' teoriyu govoryat ob ob'ektakh, opisivaemikh v etoj teorii. Naprimer, teoriya grupp, teoriya mnozhestv i t.d.

Schitaetsya, chto sozdanie matematicheskoj teorii yavlyaetsya prerogativoj matematikov. Interesnij vopros: naskol'ko sozdanie matematicheskoj teorii mozhet bit' avtomatizirovano?

Razvitie formal'nikh metodov v matematike i sovershenstvovanie vichislitel'noj tekhniki pozvolilo razrabotat' programmi, realizuyuschie deduktivnie sistemi, v chastnosti napravlennie na dokazatel'stvo teorem. V knige rassmatrivaetsya matematicheskoe i programmnoe obespechenie, pozvolyayuschee stroit' dostatochno slozhnie deduktivnie sistemi, v tom chisle matematicheskie teorii.

V nauke i na praktike chasto vstrechayutsya sistemi, kotorie mozhno opisat' sleduyuschim obrazom: imeetsya nekotoroe kolichestvo iskhodnikh ob'ektov i nekotoroe kolichestvo pravil postroeniya novikh ob'ektov iz iskhodnikh i uzhe postroennikh. Ili tak: imeetsya nachal'naya pozitsiya (nachal'noe sostoyanie) i zadani "pravila igri" (pravila perekhoda ot sostoyanij k sostoyaniyam). Takie sistemi nazivayutsya deduktivnimi ili ischisleniyami.

Zadacha zaklyuchaetsya v postroenii deduktivnoj sistemi i formal'nogo yazika, kotorie opisivayut kak matematicheskie ob'ekti, tak i utverzhdeniya ob etikh ob'ektakh, t.e. teoremi i aksiomi. Nuzhno razrabotat' algoritm, realizuyuschij sistemu avtomaticheskogo postroeniya matematicheskikh virazhenij, ikh analiza i perevoda na estestvennij yazik. Virazheniya mogut bit' dvukh tipov. Odni opisivayut matematicheskie ob'ekti, drugie -- viskazivaniya ob ob'ektakh. Suschestvuet neskol'ko podkhodov, kotorie ispol'zuyutsya pri postroenii matematiki -- eto teoretiko-mnozhestvennij, konstruktivnij (algoritmicheskij), teoriya toposov i dr. Matematicheskaya logika tozhe yavlyaetsya chast'yu osnovanij matematiki. I pri postroenii matematicheskikh teorij mozhno rassmatrivat' razlichnie logiki (intuitsionistskuyu, modal'nuyu i dr.). Deduktivnaya sistema, kotoraya budet stroit'sya, ispol'zuet klassicheskuyu logiku predikatov pervogo poryadka. V kachestve iskhodnogo ob'ekta rassmatrivaetsya predikat prinadlezhnosti. Produktami vivoda etoj deduktivnoj sistemi yavlyayutsya matematicheskie ponyatiya i teoremi. Vzyatie vmeste eti ponyatiya i teoremi obrazuyut matematicheskuyu teoriyu. Razrabotan i realizovan na komp'yutere algoritm, sootvetstvuyuschij deduktivnoj sisteme.