1. |
Паскевич А.Ю. Засоби формалізації математичних знань та міркувань: теоретичні та практичні аспекти: Автореф. дис... канд. фіз.-мат. наук: 01.05.01 / А.Ю. Паскевич ; Київ. нац. ун-т ім. Т.Шевченка. — К., 2005. — 20 с. — укp.На базі мови TL розвинуто формальну мову подання математичних текстів ForTheL, що є близькою за синтаксисом до природної англійської мови і може бути перекладена в мову першого порядку. Сформульовано поняття коректності тексту у мові ForTheL. Запропоновано оригінальне поняття істинності твердження у деякій позиції всередині формули першого порядку та досліджено його властивості. Доведено, що за умов еквівалентності двох формул, що є локально істинною у заданій позиції, ці дві формули є взаємозамінюваними у цій позиції. Відзначено, що поняття локальної істинності дозволяє обгрунтувати коректність різноманітних перетворень складних формул, а саме: розкриття визначень або додання допоміжних тверджень всередині формули. Запропоновано процедуру породження "відомостей" про окремі входження термів у досліджуваний ForTheL-текст; ці відомості є літерами, локально істинними у відповідному входженні, зокрема, вони несуть інформацію про тип терму. На базі цього апарату сформульовано декілька високорівневих схем доведення, які становлять "інструментарій" міркувальника. Проведено дослідження цілекерованих процедур пошуку виведення, що використовуються у програмі "Алгоритм Очевидності". Запропоновано нове доведення коректності поняття допустимої підстановки. Викладено цілекероване табличне числення, що оперує несколемізованими формулами. Доведено, що виведення у цьому численні можуть бути перетворені у виведення у класичному табличному диз'юнктному численні Model Elimination. Доведено можливість зворотнього перетворення. Запропоновано нове табличне цілекероване числення з лінивою парамодуляцією для класичної логіки першого порядку з рівністю, доведено його повноту. Скачати повний текст Індекс рубрикатора НБУВ: З973-018.210 + Шифр НБУВ: РА340396
Рубрики:
|