На базі мови TL розвинуто формальну мову подання математичних текстів ForTheL, що є близькою за синтаксисом до природної англійської мови і може бути перекладена в мову першого порядку. Сформульовано поняття коректності тексту у мові ForTheL. Запропоновано оригінальне поняття істинності твердження у деякій позиції всередині формули першого порядку та досліджено його властивості. Доведено, що за умов еквівалентності двох формул, що є локально істинною у заданій позиції, ці дві формули є взаємозамінюваними у цій позиції. Відзначено, що поняття локальної істинності дозволяє обгрунтувати коректність різноманітних перетворень складних формул, а саме: розкриття визначень або додання допоміжних тверджень всередині формули. Запропоновано процедуру породження "відомостей" про окремі входження термів у досліджуваний ForTheL-текст; ці відомості є літерами, локально істинними у відповідному входженні, зокрема, вони несуть інформацію про тип терму. На базі цього апарату сформульовано декілька високорівневих схем доведення, які становлять "інструментарій" міркувальника. Проведено дослідження цілекерованих процедур пошуку виведення, що використовуються у програмі "Алгоритм Очевидності". Запропоновано нове доведення коректності поняття допустимої підстановки. Викладено цілекероване табличне числення, що оперує несколемізованими формулами. Доведено, що виведення у цьому численні можуть бути перетворені у виведення у класичному табличному диз'юнктному численні Model Elimination. Доведено можливість зворотнього перетворення. Запропоновано нове табличне цілекероване числення з лінивою парамодуляцією для класичної логіки першого порядку з рівністю, доведено його повноту.

  Завантажити