У поданій статті запропонована нова методика статистичного дослідження ПДС-алгоритмів для важковирішуваних комбінаторних задач, на підставі якої визначається статистична значимість поліноміальних підкласів, що виділяються поліноміальною складовою ПДС-алгоритмів, та галузь їх ефективного застосування. Визначаються статистичні параметри, що дозволяють знаходити умови застосування ПДС-алгоритму, який був побудований для однієї важковирішуваної комбінаторної задачі, як ефективний засіб розв'язання інших задач з класу NP.

Доведено дві теореми, які дозволяють у класичній задачі Штейнера множину заданих точок на площині за певних умов розбивати на підмножини, на яких вихідна задача розв'язується незалежно. Це дозволило будувати кращі еврістичні алгоритми для розв'язання задачі.

Розглянуто питання програмування в сучасній системі комп'ютерної алгебри Mathematika. Описано базові об'єкти, зокрема: символи, контексти, спеціальні об'єкти, числа, символьні рядки. Висвітлено вхідний синтаксис, операції над елементами списку, теоретико-множинні операції над списками, оператори процедурного програмування, стандартну процедуру обчислень виразів у Mathematica.

Рассмотрены вопросы программирования в современной системе компьютерной алгебры Mathematika. Описаны базовые объекты, в частности: символы, контексты, специальные объекты, числа, символьные рядки. Освещены входящий синтаксис, операции над элементами списка, теоретико-множественные операции над списками, операторы процедурного программирования, стандартная процедура вычислений выражений в Mathematica.

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

Запропоновано сучасне бачення програми "Алгоритм очевидності" (Evidence Algorithm, EA), яке грунтується на аналізі поточного стану робіт з інтеграції числових викладок, аналітичних перетворень та автоматизації міркувань. Показано, що це бачення EA не тільки відповідає інтеграційним тенденціям, а й дозволяє говорити про евіденціальні парадигми.

Зазначено, що "континуум розумності" проблемно-орієнтованих інформаційних систем - це неперервно зростаюча множина системотвірних засобів - знань про предметну область, механізмів та інструментів "розумної" підтримки та забезпечення процесів прийняття рішень, виявлених і сформованих в інтерактивних процесах аналізу результатів діяльності системи. Розглянуто системотвірні засади створення, формування та використання "континууму розумності". Мова йде про інтерактивні процедури індуктивного виводу, які на підставі нагромаджених експериментальних даних дозволяють виявити невідомі раніше залежності між параметрами - показниками діяльності. Запропоновано певний формалізм процедур індуктивного виводу.

Запропоновано новий підхід щодо обгрунтування справедливості гіпотези Гільберта-Поллака, яка висловлена про оцінку відношення довжини мінімального дерева Штейнера до довжини мінімального остовного дерева на множині точок площини. За допомогою введення підходящих параметрів задача зводиться до задачі нелінійного програмування.

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

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

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

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

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