Описано цикл робіт щодо реалізації ініційованої В. М. Глушковим ще у 60-х рр. програми "Алгоритм Очевидності", які плануються з точки зору нового рівня розуміння та у відповідності до нових тенденцій у галузі інформаційних технологій і комп'ютерних наук.

Описано підхід до автоматизованого пошуку доведень теорем у середовищі цілісного математичного тексту. Підхід базується на секвенційному логічному численні першого порядку, яке містить формальні аналоги таких звичайних у математиці засобів пошуку доведень теорем, як розкриття означень та застосування допоміжних тверджень або лем.

Описано результати сучасних досліджень, проведених за програмою автоматизації доведень теорем, ініційованою В. М. Глушковим у 1960-х рр. і названою "Алгоритм Очевидності". Представлено засоби мовної та дедуктивної підтримки даної програми.

Розглянуто деякі теоретичні та прикладні питання розпаралелювання обчислень.Обговорено можливі формалізації таких понять, як обчислювальна середа та програма. У вибраній формалізації використано поняття програми за Скоттом. Одержана формалізація використовується для конструювання ефективного алгоритму розпаралелювання виконання програм, який можна реалізувати на практиці.

Вирішено проблему побудови ефективних цілеорієнтованих секвенційних числень для класичної логіки першого порядку (без рівності). Наведено результати їх коректності та повноти. Встановлено зв'язок цих числень з вхідною резолюцією, яка є неповною у загальному випадку, що задана у вигляді SLD-резолюції для дерев спеціального вигляду (SLD-дерев). Цей зв'язок надає простий спосіб побудови повного у загальному випадку розширення SLD-резолюції за рахунок додання до SLD-резолюції так званого правила контрарного закриття, яке може бути легко запрограмоване в інтелектуальні системи, що використовують SLD-техніку та потребують її повного розширення на випадок формул довільного вигляду.

Описано логічний формалізм, який є частиною так званої евіденціальної парадигми автоматизованого доведення математичних теорем, запропонованої В. М. Глушковим у вигляді комплексної програми робіт "Алгоритм Очевидності". Наведено базові секвенційні числення та дано результати коректності й повноти числень, використаних у разі імплементації системи автоматизації дедукції.

Представлено стислий опис теперішнього стану системи автоматизації дедукції (САД), а також проблеми, з якими стикаються під час роботи з цією системою. Більш докладно розглянуто мовні проблеми. Система автоматизації дедукції грунтується на принципах евіденційної парадигми автоматизації математичної діяльності. На цій парадигмі базується програма "Алгоритм очевидності" (Evidence Algorithm). Система САД призначена для інтелектуальної обробки математичних текстів, такої, як автоматичне доведення теорем і верифікація текстів, записаних на ForTheL, формальній математичній мові, яка є наближеною до природної мови математичних публікацій. На сьогодні систему САД можна використовувати для встановлення вивідності секвенцій у класичній логіці першого порядку, пошуку доведень теорем у ForTheL-середовищі та верифікації замкнених ForTheL-текстів.

Рассмотрены вопросы распределенной обработки информации в современных компьютерных системах дедуктивной поддержки научной и образовательной деятельности. Описаны опыт, накопленный в ходе разработки системы автоматизации дедукции, и трехуровневая организация обработки компьютерных знаний в системах автоматизации рассуждений.

Исследована возможность построения теоретико-множественных моделей теории лямбда на базе понятий слабо и сильно непрерывной функции. Доказано, что отталкиваясь от понятия слабо непрерывной функции, нельзя построить модели теории лямбда с помощью метода Скотта, однако родственное ему понятие сильно непрерывной функции, наоборот, ведет к построению новых лямбда-алгебр и лямбда-моделей.

Рассмотрен вопрос о том, как, умея совершать какие-то действия на произвольной совокупности событий, следует совершать аналогичные действия на нечетких множествах, представляющих прогнозы относительно этих событий. Для того, чтобы найти ответ на поставленный вопрос, разработан специальный понятийный аппарат, в рамках которого сформулировано понятие нечеткой задачи и приведена процедура, позволяющая находить решения нечетких задач. Приведены убедительные доводы в пользу корректности этой процедуры.

Рассмотрены основные парадигмы обработки математических знаний и обозначено место среди них систем Theorema и автоматизация дедукции. Описаны сравнительный анализ систем, общие черты их построения и различие в методах обработки данных.

Індекс рубрикатора НБУВ: З973-018.21

Рубрики:

Комп'ютери та програмування

Шифр НБУВ: Ж29144 Пошук видання у каталогах НБУВ