Розглянуто застосування автоматичного доведення теорем як методологічної основи нечіткого ситуаційного пошуку рішень.

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

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

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

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

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

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

Розглянуто нове обгрунтування для одержання висновків в системах з протиріччями. Доведено основні правила висновків та теорему про повноту системи обчислювання у вузькому розумінні. Запропонований підхід можна взяти за основу створення систем обгрунтування заперечуючих і ненадійних рішень, наприклад при проектуванні інтелектуальних роботів і експертних систем.

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

Розглянуто проблематику застосування засобів автоматичного доведення теорем для дослідження моделей контролю доступу на базі ролей. Запропоновано шляхи представлення моделей стандарту ANSI-INCITS 359-2004 Role Based Access Control як теорій першого порядку, дослідження їх властивостей та генерації авторизаційних рішень за допомогою ПЗ EProver.