|
-
Ключові слова:
математичне доведення, математическое доказательство ; формальна логіка, формальная логика ; автоматизація, автоматизация
-
Анотація:
У даній роботі описано підхід до автоматизованого пошуку доведень математичних теорем, особливістю якого є те, що пошук доведення здійснюється на базі цілісного математичного тексту, який записано формальною мовою першого порядку, близькою до мови математичних публікацій, що дає можливість використовувати формальні аналоги таких природних способів доведення як застосування означень понять та допоміжних тверджень у поєднанні з процедурами пошуку виводу у логічних численнях (а саме, з добре відомою процедурою негативної гіперрезолюції). Особливості підходу створюють можливість для оптимізації перебору при пошукові доведень математичних теорем.
-
Є складовою частиною документа:
-
Теми документа
-
Персоналії // Глушков Віктор Михайлович (1923-1982), Глушков Виктор Михайлович (КУ)
-
Окремі фонди та колекції КНУ // праці авторів КНУТШ, труды авторов КНУТШ, работы авторов КНУТШ
|
