Все выпуски

В данной работе представлен новый подход к интерпретации логических формул для синтеза алгоритмов и программ. Предложенный метод сочетает в себе черты реализации Клини и интерпретации Гёделя «диалектика», но не опирается на них непосредственно. Рассматривается простой вариант позитивного языка логики предикатов без функций, с конъюнкцией, дизъюнкцией, импликацией и кванторами всеобщности и существования. Описана новая реализационная семантика формул и секвенций, в которой рассматривается не просто реализация формулы, а реализация с дополнительной поддержкой. Реализация примерно соответствует реализации Клини. Поддержка предоставляет дополнительные данные в пользу того, что реализация корректна. Поддержка должна подтвердить, что реализация работает корректно для формулы в любых корректных условиях применения. Представлен язык доказательств, для которого доказана теорема о корректности, показывающая, что любая выводимая секвенция имеет реализацию и поддержку, подтверждающую, что эта реализация работает правильно для этой формулы в любых корректных условиях при подходящем интерпретаторе используемых программ.

Под термином «размыкание предиката» понимается сведение задачи поиска и изучения свойств множества истинности заданного предиката к задаче поиска и изучения свойств неподвижных точек некоторого отображения. Размыкание предиката дает дополнительные возможность анализа его множества истинности, а также позволяет строить элементы этого множества с теми или иными свойствами. Известны примеры размыкания нетривиальных предикатов, таких как предикат «быть стабильным (слабо инвариантным) множеством», предикат «быть неупреждающим селектором», предикат «быть седловой точкой», предикат «быть равновесием Нэша». В упомянутых случаях вопрос об априорной оценке возможности размыкания того или иного интересующего нас предиката и о построении соответствующего размыкающего отображения оставался за рамками рассмотрения: размыкающие отображения предоставлялись как готовые объекты. В предлагаемой заметке мы постараемся отчасти закрыть этот пробел: приводятся формальное определение операции размыкания предиката, способы построения и исчисления размыкающих отображений и их основные свойства. Описываемый подход примен\'им во всех упомянутых выше положительных примерах. В качестве иллюстрации проведено следующее этому способу построение размыкающего отображения для предиката «быть нэшевским равновесием».

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

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

В работе разрабатывается метод, именуемый «размыкание предиката», сводящий задачу поиска множества истинности предиката к задаче поиска множества неподвижных точек некоторого (вообще говоря, многозначного) отображения. Предлагаемая техника дает дополнительные возможности анализа задач и построения решений путем систематического привлечения результатов теории неподвижных точек. Даны формальное определение операции размыкания предиката, способы построения и исчисления размыкающих отображений и их основные свойства. В случае когда область определения предиката частично упорядочена, указаны способы построения размыкающих функций, обладающих свойством сужаемости. Это позволило получить представления интересующих элементов решения в виде итерационных пределов. Предлагаемый подход в силу абстрактности имеет широкую сферу применения. Вместе с тем эффективность полученного решения зависит от специфики рассматриваемой задачи и выбранного варианта реализации метода. В качестве иллюстрации в работе рассмотрена процедура построения размыкающего отображения для предиката «быть неупреждающим селектором». На основе этого отображения получено выражение для наибольшего неупреждающего селектора заданной мультифункции.

В статье определяются и исследуются основные конструкции и семантика языка описания действий (action description language), предназначенного для описания и анализа преобразований отношений моделей ситуаций (реляционных преобразований).
Основное отличие описываемого языка KSL (Knowledge Specification Language) от традиционных (STRIPS, ADL, PDDL и т. п.) - использование кроме традиционных (STRIPS-like) правил их теоретико-множественных композиций. Это существенно повышает выразительность языка.
Точная характеризация основных свойств реляционных преобразований на языке логики предикатов первого порядка (FOL), но без использования дополнительных конструкций ситуационного исчисления, дает возможность сформулировать и доказать естественный критерий реализуемости (непротиворечивости) системы правил реляционных преобразований и, соответственно, явно описывать и исправлять логические противоречия рассматриваемой системы преобразований.

Исследуются методы представления отношений предикатами Радемахера, предлагается метод коллективного голосования для распознавания отношений.