автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.17, диссертация на тему:Дедуктивный синтез алгоритмов с учетом вычислительных ресурсов
Автореферат диссертации по теме "Дедуктивный синтез алгоритмов с учетом вычислительных ресурсов"
Санкт-Петербургский государственный университет Ко 00
На правах рукописи
•¿¿нвшз
БЕЛ ЫЮ КО В Анатолий Петрович
ДЕДУКТИВНЫЙ СИНТЕЗ АЛГОРИТМОВ С УЧЕТОМ ВЫЧИСЛИТЕЛЬНЫХ РЕСУРСОВ
05.13.17 — теоретические основы информатики
АВТОРЕФЕРАТ
диссертации на соискание ученой степени доктора физико-математических наук
КОШ РОЛЬ !..;;]
, 5
' ' г | п г>
Санкт-Петербург 1993
Работа выполнена в Санкт-Петербургском государственном университете.
Научный консультант — доктор физико-математических наук, профессор Слисенко А. О.
Официальные оппоненты — доктор физико-математических наук, с. н. с. Цейтин Г„ С.; доктор физико-математических наук, профессор Летичевский А. А.; доктор физико-математических наук, профессор Замов Н. К.
Ведущее предприятие — Институт прикладной математики Российской академии наук.
Защита диссертации состоится «_» _ 199 г.
в __ час. _ мин. на заседании специализированного совета
Д 063.57.52 по защите диссертации на соискание ученой степени доктора физико-математических наук в Санкт-Петербургском государственном университета по адресу: 198904, Санкт-Петербург, Старый Петергоф, Библиотечная площадь, 2.
С диссертацией можно ознакомиться в библиотеке Санкт-Петербургского университета по адресу: 199034, Санкт-Петербург, Университетская набережная, 7/9.
Автореферат разослан «-»--199 — г.
Ученый секретарь специализированного совета
Д. А. Кубенскнн
ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ
АКТУАЛЬНОСТЬ ТЕШ. Работа посвящена исследованию некоторых вопросов, связанных с дедуктивна« синтеза« алгоритмов. Под дедуктивным синтезом ш понимаем создание алгоритмов с помощью построения конструктивных доказательств осуществимости объектов, вычисляемых этими алгоритмами. В широком смысле конструктивными считаются доказательства, обосновывавшие существование объектов путем явного указания па способы их построения. Благодаря этой особенности, конструктивное доказательство существования объекта, в суаности, содержит алгоритм его вычисления. Такой подход основан на теоретических работах, берущих начало от реализационной семантики Рейтинга - Колмогорова - Клини -Геделя (1,2,3,4] и продолжающихся многочисленными современными публикациями Сем., например, [5,6,7,8]).
Для любой практической реализации этого подхода, допускающей автоматизацию какой-либо части процесса построения алгоритмов, необходимо, во-первых, выбрать формальный язык для записи предложения о существовании объектов, которые требуется вычислять (т.е. язык формулировок теорем), во-вторых, зафиксировать способ интерпретации предложений этого языка, при котором предложениям о существовании объектов соответствуют алгоритмы их построения, в-третьих, построить формальную систему для доказательства таких предложений, в-четвертых, показать, что эта система корректна, т.е. соответствует выбранному способу интерпретации предлохений. Корректность означает, что для каждой доказанного
существования можно построить алгоритм (программу) вычисления существующего объект^ Корректность должна быть обоснована также конструкт зно. Это значит, что это обоснование должно содержать алгоритм построения упомянутых программ по доказательствам.
В некоторых случаях выбранная формальная теория настолько проста, что удается построить алгоритм, выводящий доказательство любого ее истинного предложения. В других случаях такой алгоритм невозможен. ' Последнее означает, что некоторые, доказательства необходимо, строить с творческой помощью человека, или необходимо сузить класс задач для решения. .
К частичным практическим реализациям этого подхода можно, согласно работам Г. Е. Минца и Э.Х.Тыугу [9], отнести такие системы, как ПРИЗ, разработанную под руководством Э.Х.Тыугу {10], СПОРА, разработанную под руководством С.С. Лаврова [11], СПРУТ [12], САТУРН [13]. В этих системах используются очень простые теории, что за счет сужения класса решаемых задач позволяет получить высокую степень автоматизации построения алгоритмов.
Можно отметить отличительную особенность всех упомянутых работ - невозможность задания ограничений на объем вычислительных ресурсов, используемых синтезируемыми алгоритмами.' При практичэской реализации в сложных случаях эта особенности., является недостатком: в таких системам могут синтезироваться алгоритмы, выполнение которых затруднено илк нс?воамохл:о вследствие сшаиком большой их потребности в ' у:"<у.спулепыш:< ресурсах. В настоящей работе преодолевается
этот недостаток - предлагаются теории, в которых можно задать ограничения на объем вычислительных ресурсов.
В основном, в работе строятся подходящие дедуктинние системы для синтеза различных классов алгоритмов. При этом главное внимание уделено не исследованной другими авторами возможности ограничении объемов вычислительных ресурсов, Используемых этими алгоритмами . Как правило, это - время С"процессорное") выполнения алгоритмов. Таким образом, направление, к которому относятся основные результаты данной работы, можно охарактеризовать названием "дедуктивная теория сложности алгоритмов".
Актуальность разрабатываемого направления определяется тем, что оно позволяет соединить оценки сложности вычислений н автоматизации порождения компьютерных программ дедуктивными средствами.
ДЕДЬ РАБОТЫ - создание формальных теорий, на ' основе которых можно строить системы дедуктивного синтеза программ для различных классов предметных областей, различных стилей программирования, для баз данных, учитывающих расход в процессе вычисления различных вычислительных ресурсов, таких как время вычисления.
ОБЩАЯ МЕТОДИКА ВЫПОЛНЕНИЯ ИССЛЕДОВАНИЙ. В работе используются методы теории формальных систем и методы алгоритмической теории сложности. Для объединения этих методов предложено новое понятие реализационной семантики формул на основе понятия вычислительной среды.
НАУЧНАЯ НОВИЗНА. В работе содержится ряд существенно новых результатов. Построены формальные теории,
предназначенные для дедуктивного синтеза алгоритмов с учетом в постановках задач расходуемых вычислительных ресурсов, таких, как процессорное время вычисления. Некоторые из теорий учитывают изначальную ограниченность времени, доступного для вычисления независимо от того, указано ли это в постановке задачи. Кроме этих общих теорий, построены подобные специализированные теории для синтеза программ с абстрактными типаии данных, синтеза программ анализа текстов и списков древовидной структуры. Построены методы и теории дедуктивного синтеза запросов в базах данных как с учетом эффективности запроса; так и для синтеза ЕСТЕСТВЕННЫХ запросов по их неполным ■ спецификациям с использованием релевантных конструктивных логик. Исследованы свойства реализационной полноты и непротиворечивости основных теорий. Доказаны теоремы о содержательной непротиворечивости всех теорий по отношению к приводимым для них реализационным семантикам и теоремы о содержательной полноте по отношению к этим семантикам для наиболее простых теорий. Даны некоторые сложноствыэ оценки для распознавания выводимости в теории дедуктивного синтеза запросов в базах данных.
ПРАКТИЧЕСКАЯ ЦЕННОСТЬ. Хотя данная работа носит теоретический характер, ее результаты могут быть использованы при построении практических систем дедуктивного / синтеза программ. На практике полученные результаты, относяцдеся к области баз данных были применены при построении системы управления базами данных, разработанной автором для государственного предприятия "Боткинский завод".
АПРОБАЦИЯ РАБОТЫ. Результаты работы докладывались на семинарах по алгоритмической теории сложности Петербургского отделения Математического института РАН, Всесоюзных и Межреспубликанской конференциях по матеыатическо логике, теоретической кибернетике, синтезу, верификации и отладке программ, Всесоюзном семинаре по оптимизации и преобразованиям программ и др.
ПУБЛИКАЦИИ. По теме диссертации опубликовано 15 работ, которые отрагают ее основное содержание.
СТРУКТУРА И ОБЪЕМ РАБОТЫ. Диссертация состоит из введения, трех глав, разбитых на 6 параграфов, заключения и списка использованной литературы. Объем работы - 130 стр., включая 11 страниц списка использованной литературы, насчитывающего 94 наименований.
СОДЕРЖАНИЕ РАБОТЫ
В первой главе диссертации строятся дедуктивные теории для синтеза программ с учетом вычисл.-.тельных ресурсов. Вторая глава посвящена построению аналогичных теория для синтеза программ в некоторых специальных случаях: использование абстрактных типов данных, обработка текстов. Третья глава посвящена синтезу программ, работающих с базами данных.
Первая глава начинается иллюстрацией понятия дедуктивного синтеза алгоритмов. В наиболее простой формулировке под дедуктивным синтезом алгоритмов обычно подразумевается следующая задача.
Дана формула вида
¥х(АСх) => Эу ВСх. у)), С1)
где значения переменных х и у могут быть конструктивными объектами любой сложности, например, векторами, состоящими из компонент, кс;орые можно закодировать словами в некотором алфавите.
Пусть Свойства А и В - легко проверяемые (т.е. рекурсивно разрешимые). Требуется построить конструктивное доказательство формулы (1). Такое конструктивное доказательство по определении должно прежде всего содержать способ построения объекта у со свойством ВСх,у) по каждому объекту' х со свойством А(х). Этот способ представляет собой программу для вычисления функции Г, даюцей требуемое значений у па данному х;
ухСАСх) => ВСя, Кх))). . (2)
Более того, чтобы последовательно говорить о системе конструктивных доказательств, требуется иметь алгоритм, строящий программу для функции Г из С2) по доказательствам формул вида С1).. Следовательно, любая система автоматизации •построения конструктивных доказательств подобных формул' может служить основой системы автоматического порождения программ по постановкам задач, записываемым в этом виде.
Обычно для построения конструктивных доказательств используются логические . системы без доказательств от противного, называемые интуиционистскими (например, интуиционистское исчисление предикатов [3]). Для этих систем удобно рассматривать такую интерпретацию логических предложений, при которой каждой формуле ставится в соответствие множество объектов, называемых ее реализациями.
Истинность формулы означает непустоту этого множества. В частности, функции Г из С2) можно считать реализацией формулы С1). Такая интерпретация логики называется реализационной интерпретацией. Шепча реализации доказываемых формул и извлекаются из их конструктивных доказательств.
К сожалению, применение известных подобных систем не позволяет учитывать при синтезе программ то, что некоторые из обрабатываемых объектов могут изменяться л даже разрушаться. В частности, желательно, чтобы з качестве объектов могли фигурировать процессорное время, выделенное для вычисления, другие расходуемые вычислительные ресурсы, предметы физического мира, в котором действует программируемый исполнитель. Это позволило бы включать в доказываемую формулу ограничения на объем вычислительных ресурсов, которые разрешено использовать строящейся реализации данной формулы.
Логические системы, учитывающие подобные ограничения, обычно называются релевантными логиками. В некоторых из таких логических системах одну и ту же формулу, вообае говоря, нельзя использовать использовать носгольно раз в одном и том же выводе для получения разных заключений.
Первая глава диссертации посвящена построению таких релевантных теорий.- Для интерпретации этих теорий вводится понятие вычислительной среды, в которой действует некоторый абстрактный исполнитель. Среда, с точки зрения исполнителя, представляет собой систему особых точек зхода, через которые исполнитель может на нее воздействовать. Эти точки входа связаны с некоторым обадл объектом, называемым состоянием такой среды. При практической интерпретации такой ситуации
природа точек входа может быть самой различной: это могут быть обычные натуральные одела, объекты материального мира, ресурсы (например, запасы времени для вычисления), файлы, программы, команды различный исполнительным устройствам. Исполнитель не моает наблвдать состояние среды и непосредственно воздействовать на него. Он может воздействовать аа среду только через ее входы и наблвдать упомянутые нижа результаты такого воздействия. Воздействия на среду могут быть трех родов, перечисленных ниже.
1. Можно заставить среду применить один вход к конечной последовательности других входов. Например, применить команду "привести в исходное состояние" к печатающему устройству. В результате такого применения некоторые из используемых в нем входов могут исчезнуть, но могут и появиться новые входы, причем, вариантов завершения может быть несколько. Например, печатающее устройство может оказаться выключенным, т.е. исчезнет "печатающее устройство" и появится "выключенное печатающее устройство", в другом случае вместо печатающего устройства появится "печатающее устройство в исходном состоянии". Среда сообщает исполнителю номер варианта завершения процесса и передает в распоряжение исполнителя сохранившиеся и вноъь появившиеся входы. В нашем примере номер варианта - 1 или 2. Передаваемый вход . - устройство в выключенном или исходном состоянии, в зависимости от варианта. Входы, которые можно применять к другим входам называются процедурами.
2. Можно заставить среду создать копию одного из входов. Входы для которых это возможно, называются копиуемыми.
Примеры копируемых входов: команда "привести в исходное состояние", натуральное число 1. Примеры некопируемых входов: "печатающее устройство", "запас времени для работы в 100 шагов".
3. Можно научить среду действовать по заранее составленной программе, используя специально резервируемые для •этой программы входы. Это называется построением нового входа. В качестве языка программ для вычислительной среды в настоящей работе использован специальным образом модифицированный язык машин Тьюринга. Пример составного входа - процедура выдачи документа на зарезервированных для этой цели пяти листах бумаги. Конечно, количество зарезервированных входов шкет быть и нулевым.
Для формулирования задач в такой вычислительной среде разработан специальный логический язык, любая формула которого обозначает, кроме предложения, некоторый тип данных, содержание которого меняется с преобразованием среды. Истинность формулы означает, что этот тип данных не пуст. Это и есть реализационный смысл формулы. Формула имеет один из следующих трех видов:
1) P(x,...,z), где x,..,z - переменные, Р - предикат; эта формула обозначает'настраиваемый тип данных Р с указанными параметрами х, ... , z (при подстановке конкретных входов
вместо х.....z получается конкретный тип данных), а такке
предложение о непустоте этого типа;
2) !А, где А - формула, эта формула обозначает множество копируемых элементов типа данных А, а также непустоту этого множества;
3) (а: А.....с;С => |Ь:В.....б:0|...(в:Е.....д:Ю, где
а, ,,. ,с, Ь..... б.....е, ... , д - переменные,
А.....С,В.....О,... ,Е,...,6 - формулы; эта формула обозначает
тип процедур с аргументами ' а.....с типов А,..,С
соответственно, в результате выполнения которых ыохет получиться одна из последовательностей объектов от Ь,..,б с типами В,...соответственно до е,...,д с типами Е,...,С соответственно; эта формула также обозначает что для любых упомянутых аргументов осуществима одна из упомянутых последовательностей результатов; эта формула представляет крупноблочную логическую связку и заменяет собой известные логические связки: конъюнкцию, дизъюнкцию, импликацию, отрицание, кванторы.всеобщности и существования.
Запись вида а:А, где а - переменная, А - формула, называется формой. Введено понятие интерпретации некоторой Системы форы в рассмотренной вычислительной среде. При этом кавдой форме а: А ставится в соответствие вход среды. Данный вход называется ■ реализацией формулы А. Определены способы совместного преобразования системы форм и интерпретирующей ее вычислительной среды. С преобразованием вычислительной среды некоторым естественным образом связывается соответствующее ему преобразование интерпретируемой системы форм. Корректность интерпретации заключается в определенной, согласованности этих преобразований. Формула называется реализуемой в данной корректной интерпретации системы форм в вычмслительной среде, если эту интерпретацию можно преобразовать так, чтобы один из входов данной среды бал реализацией указанной формулы.
Предлагаемый язык позволяет непосредственно в спецификации строящегося алгоритма задавать, например, временную слояюсть его выполнения. Для этого достаточно ввести такой одноместный предикат Т, что формула ТСп) в вычислительной среде интерпретируется входом, который представляет собой запас из п шагов времени для вычисления. Пусть (Н - формула, обозначающая тип натуральных »шеел. Тогда формула
Сп.ЕМ,а: АСп), I: ТСп) => |Ь: ВСп,а)) будет означать, что имеется программа, вычисляющая значение ВСп,а) по натуральному числу п, объекту а типа АСп) за п иагов времени.
Необходимо отметить, что, хотя строящаяся теория может иметь дело со временем, как и временные логики [14], но она сама не является временной логикой и представляет собой другой подход к этой проблеме. Главное отличие состоит з том, что время рассматривается как вычислительный ресурс, а не как фактор синхронизации процессов.
Построена формальная теория, в которой доказуемы некоторые из определенных выше формул. Основной результат первого параграфа - теорема о содержательной полноте и непротиворечясвостя построенной теории для рассматриваемых интерпретаций.
Второй параграф приближает пас к реальной действительности. Дело в том, что теория и интерпретации, рассматриваемые в первом параграфе никак не учитывают изначальную ограниченность ресурса времени, которая имеет
- и -
место во всех практических случаях, Изменение интерпретации и теории позволяет охватить к этот случай.
Для этого, кроме вычислительной среды без ограничений, во втором параграфе построены еще два варианта вычислительной среды:
- среда с ограниченным временем,
- среда с ограниченной памятью.
В первом случае предполагается, что с каждым входом вычислительной среды может Сыть связано определенное количество (выраженное натуральным числом) особого вычислительного ресурса, называемого временем вычисления. Общ 1 количество входов н суммарное время в среде конечно. После каждого применения одного входа к другим суммарное время уменьшается по крайней мере на единицу. Отсюда следует, что общее число применений одних вводов к другим в такой среде ограничено.
Во втором случае к такому ограничению времени добавляется ограничение допустимого обьема памяти машины Тьюринга. которая, как было указано выше, выпошеняет программы составных входов в этой среде.
Для каждого из этих вариантов построены формальная система для вывода формул, имеющих реализации при любой корректной интерпретации в любой среде. Доказаны соответствующие теоремы о непротиворечивости. Для второго случая доказана теорема о полноте. Для первого случая доказана невозможность полной аксиоматизации теории.
Построение теорий и их интерпретаций продолжается во второй главе диссертации - в параграфах 3 и 4.
В третьем параграфе рассматриваемые теории пополняются средствами, соответствующими в программировании абстрактным типам данных с сохранением содержательной непротиворечивости.
В четвертом параграфе строятся аналогичные теории для синтеза алгоритмов обработки текстов и списков на языке, подобном языку РЕФАЛ [15].
Пятый и шестой параграфы диссертации, составляют третью главу, посвященную вопросам синтеза алгоритмов в базах данных.
В пятом параграфе рассматривается задача порождения алгоритмов запросов в базах данных, поддерживаемых в реальное время. Идея постановки задачи состоит в том, что по данному алгоритму вычисления функции Г над базами данных требукется построить быстрый алгоритм вычисления функции д,
определяемой равенством:
д(ГС х),Дх)=ГС х+Дх). На практике, однако, естественно решать на столь аестко поставленную задачу. Достаточно уметь построить, кроме д, такие функции Г' и быстро вычислимую п, что
. дСГСх),ДхЭ*ГСх+Дх) и ГСх)=гг(ГСх)). Понятие "быстрой" вычислимости формализуется в виде вычислимости в реальное время. В указанном параграфе получен и обоснован способ дедуктивного порождения таких функций Т, для которых рассматриваемая задача разрешима. Причем, получен алгоритм построения программ для д.
В шестом параграфе рассматривается задача дедуктивного синтеза алгоритмов "естественных" запросов к базе данных. Понятие естественности запроса на неформальном уровне заключается в требовании отсутствия сопоставления в нем не
связанных между собой данных. Другими словаки, запрос не должен создавать структуру данных, некоторые фрагменты которой основываются на сочетаниях никак не зависящих друг от друга элементах входных структур. Бессмысленным, например, является требование выдать сумму произведений всех возможных окладов на все возможные времена работы. Это требование естественности создает некоторую избыточность в полной записи алгоритма запроса. Такую избыточность можно использовать для сжатой записи запросов. В сущности, вместо запроса используется его спецификация. Предложена формальная теория, позволяющая восстанавливать алгоритм запроса по его спецификации. Эта теория может служить формализацией понятия "естественности" запроса. Исследования параграфа 6 имеют некоторое родство с исследованиями по дедуктивным базам данных 116-18]. 'Основное отличие состоит в том, при предложенном подходе дедуктивный аппарат используется ие ва время выполнения запросов к базам данных, а исключительно при их предварительной обработке, не увеличивая, таким образом, время выполнения запросов. При это-дедукция применяется ие для вывода данных, а для вывода самих запросов.
ЛИТЕРАТУРА
1. Keytlng. Materoatische Grundlagenforschung, Intuitionisraus, Beweisstheoriô // Ergebnisse der Hath, etc. III, 4, Berlin, 1934.
2. Kolmogorov. 2ur Deutung der Intuitionistischen Logik //
Math Zeitschrift, 1932, 25, P.53-65.
3. Клики С.К. Введение в метаматематику, и., 1957.
4. Godel К. über eine bisher noch nicht benutze Erweiteung
des finiten Standpunktes // Lialectica 12, 1958, ЪЗ/4, P. 280-287.
5. Constable R. L. Constructive mathematics and automatic
program writers // Information Processing 71, North Holland, 1972, v. 1, Pi 229-233.
6. Kreisel G. Some uses of proof theory for findina computer
programs // Colloc. Intern. Log., Clerracnt-Ferrant, • 1975, P. 151.
7. Uepejvoda IJ. N. The logical approach to programming. //
Lect. Hotes Comp. Sei., 3881, 118, P.261-290.
8. Nepejvoda K.N. The connection between the proof theory
and conputer programming // 6-th Intern. Congr. of Logic, Methodology and Philosophy of Science, Hannover, 1979, v.l. P.7-11.
9. Минц, Г. E., Тыугу Э. X. Обоснование структурного синтеза
программ // Автоматический синтез программ, Таллин, 1983, С. 5-40.
10. Каяро М. И. , Калья А. И., Тыугу Э. X. Инструментальная
система программирования ЕС ЭВМ (ПРИЗ), И. 1981. И. Бабаев И.О., Лавров С.С. и др. СПОРА - система с
автоматическим синтезом программ // Применение методов-, математической логики, Таллин, 1983, С. 29-41.
12. Гайдамакина С. П., Дагалдьян А. А., Кузнецова В. А. , Е.В.Натагаон, Т.Е.Романова Организация синтеза программ в системе СПРУТ // Синтез, тестирование, верификация и отладка программ: Тезисы докладов всесоюзной научной конференции, Рига, 1981, С.70-71.
13. Опарин Г.А., Феоктистов Д.Т. САТУРН - метасистема для автоматизации конструирования и поддержки функционирования пакетов прикладных программ с автоматическим планированием вычислительного процесса // Пакеты прикладных программ, итоги и применения, Новосибирск, 1985, С.12-21.
14. Long D. A review of temporal logics // Know. Eng. Rev, 1989, 4, N 2. P. 141-162.
15. Турчин Ф.В. Программирование на языке РЕФАЛ // Препринты
Инст. прикл. матем. АН СССР, 1971, N 41, 43, 44. 48, 49.
16. Gallaire Н., Minker J., Nicolas J.-M. Logic and databases: a deductive approach // ACM Computing Surveys, Vol.16; Ho.2, 1984, P.153-185.
17. Nicolas J. -M., Gallaire H. Data base: theory vs. interpetation // Logic and databases / H. Gallaire, J.Minker Ceds.3, Plenum Publishing Corporation, 1978, P. 33-54.
18. Reiter R. , Towards a logical reconstruction of relational
database theory // On conceptual modelling / M. L. Brodie, J.Mylopoulos, J. W. SchmidtCedSi), Springer, 1984, P. 191-233.
РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ
1. Бельтюков А. П. Язык запросов, поддерживаемых в реальное
время // Проблемы теоретической кибернетики. Тезисы докладов VII Всесоюзной конференции (июль 1988г.Э, Горький, 1988, С. 45-46.
2. Бельтюков А.П. Машинно-независимое описание класса запросов, поддергиваемых в реальное время // Математические методы построения и анализа алгоритмов, Ленинград, "Наука", 1990, С. 16-25.
3. Бэльтюхов А. П. Формальная теория для порождения
. правильных программ заданной вычислительной сложности.// Всесоюзная конференция "Методы математической логики в проблемах искусственного интеллекта и систематическое программирование", Вильнюс, 1980, Часть 1, С. 64-66.
4. Бельтюков А. П. Дедуктивный синтез рефал-программ
контролируемой вычислительной сложности // Синтез, тестирование, верификация и отладка программ. Тезисы всесоюзной научной конференции, Рига, 1981, С.35-36.
5. Бельтюков А.П. Язык дедуктивного программирования. //
Теория языков программирования: Сб. научн. трудов, Удмуртский гос. университет, Ижевск, 1S83, С. 3-18.
6. Бельтюков А.П. Сложностяая логика. // 6-я Всесоюзная
конференция по математической логике: Тезисы докладов. Изд. Тбилисского ун-та. Тбилиси, 1932, С.18.
7. Бельтюков А.П. Дедуктивная оптимизация программ. //
Оптимизация и преобразования программ: Материалы
всесоюзного семинара, Новосибирск, 1983, Часть 1, С. 105-113.
8. Бельтюков А.П. Абстрактные типы данных в .дедуктивной
программировании // Конструктивные процессы: Тезисы конференции, Ижевск. 1984, С.34-36.
9. Бельтюков А.П. Логика прерываний // VII Всесоюзная
конференция "Проблемы теоретической кибернетики", 18-20 сентября 1985 г.: Тезисы докладов, Иркутск, 1985, Часть 1, С. 22-23.
10. Бельтюков А. П. Логика вычислительного процесса с откатами // Девятая всесоюзная конференция по ...атематической логике, Ленинград, 1988, С. 17.
11. Бельтюков А.П. Логика баз данных. // Математическое
моделирование и информационные технологии: Межвузовский сборник научных трудов. Ижевск 1991, С.80-91.
12. Бельтюков А.П., Дедуктивный синтез алгоритмов просмотра баз данных // Восьмая всесоюзная конференция по математической логике: Тезисы докладов, М., 1986, С.17.
13. . Bel'tyukov, А.P.. A formalization of database natural
request notion // Summer school and conference on Mathematical Logic, Sofia, 1988, P. 8,
14. Бельтюков А.П. Базы данных, ориентировашшы на работу с
помощью непроцедурного языка // Синтез программ: Тезисы докладов школы-семинара. Устинов, 1985, С. 57-КЗ.
15. Бельтюков А. П. Формальная конструктивная теория для синтеза алгоритмов в среде с ограничением времени. // XI межреспубликанская конференция по математической логике: Тезисы сообщений, Казань, 1992, С.21.
-
Похожие работы
- Методика и средства интеллектного контроля и преобразования данных для вычислительного эксперимента в исследованиях энергетики
- Функциональный поход к концептуальному программированию
- Средства и методы ускорения дедуктивного вывода в информационных системах с большим объемом данных
- Поддержка развитых логических языков запросов в дедуктивных базах данных
- Поддержка развитых логических языковзапросов в дедуктивных базах данных
-
- Системный анализ, управление и обработка информации (по отраслям)
- Теория систем, теория автоматического регулирования и управления, системный анализ
- Элементы и устройства вычислительной техники и систем управления
- Автоматизация и управление технологическими процессами и производствами (по отраслям)
- Автоматизация технологических процессов и производств (в том числе по отраслям)
- Управление в биологических и медицинских системах (включая применения вычислительной техники)
- Управление в социальных и экономических системах
- Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей
- Системы автоматизации проектирования (по отраслям)
- Телекоммуникационные системы и компьютерные сети
- Системы обработки информации и управления
- Вычислительные машины и системы
- Применение вычислительной техники, математического моделирования и математических методов в научных исследованиях (по отраслям наук)
- Теоретические основы информатики
- Математическое моделирование, численные методы и комплексы программ
- Методы и системы защиты информации, информационная безопасность