Системы переписывания формул и их применение в автоматической верификации программ тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Ануреев, Игорь Сергеевич

• Ануреев, Игорь Сергеевич
• кандидат физико-математических наук
• 1998

Оглавление диссертации кандидат физико-математических наук Ануреев, Игорь Сергеевич

Содержание

Введение

1 Теория систем переписывания формул

§1 Основы теории систем переписывания термов

§1.1 Абстрактные системы редукций

§1.2 Системы переписывания термов

§1.3 Техника сужения

§2 Системы переписывания формул

§2.1 Основные определения

§2.2 Корректность систем переписывания формул

§2.3 Проблема нетеровости

§3 Завершимость систем переписывания формул

§3.1 Системы элиминации анализаторов

§3.2 Системы элиминации анализаторов со статусом 42 §3.3 Системы элиминации анализаторов с базой подстановок

2 Применение систем переписывания формул в автоматическом доказательстве

§1 Разрешимые теории

§1.1 Арифметика Пресбургера и ее расширения

§1.2 Теории равенства и частичного порядка

§1.3 Теория равенства мультимножеств

§2 Особенности применения систем переписывания формул в многосортных теориях

§2.1 Сорта, определяемые обобщенными конструкторами :

§2.2 Корректность систем переписывания формул

§2.3 Булевский сорт

§3 Разрешающие процедуры, основанные на системах

переписывания формул

§3.1 Фрагменты теории целых чисел

§3.2 Фрагменты теории множеств

§3.3 Фрагменты теории мультимножеств

§3.4 Фрагменты теории кортежей

3 Применение систем переписывания формул в автоматической верификации программ

§1 Предварительные съедения о верификации

§1.1 Метод Хоара

§1.2 Система верификации СПЕКТР

§1.3 Модельный язык аннотированных программ

§2 Элиминация операций над структурами данных

§2.1 Последовательные файлы

§2.2 Массивы

§3 Модуль переписывания формул в системе СПЕКТР

§3.1 Общая структура модуля

§3.2 Тактикалы

§3.3 Результаты эксперимента

§4 Примеры автоматической верификации программ

§4.1 Программы редактирования текстов

§4.2 Сортировка массивов

§4.3 Сортировка файлов естественным слиянием

Заключение

Литература

Введение диссертации (часть автореферата) на тему «Системы переписывания формул и их применение в автоматической верификации программ»

Введение

В создании надежного программного обеспечения — важнейшей задачи технологии программирования — значительное место занимает классическая верификация программ [1, 21, 22, 31, 37, 73. 105, 132], основы которой были заложены в работах Флойда и Хо-ара. При этом решающую роль для автоматизации процесса верификации программ играет разработка методов автоматического доказательства, ориентированных на верификацию. Выделим методы и техники автоматического доказательства, которые используются в настоящее время в системах верификации. При рассмотрении методов и техник автоматического доказательства будем сравнивать их по следующим характеристикам:

- Ориентированность на верификацию, заключающаяся в том. учитывают ли разрешающие процедуры, основанные на том или ином методе или технике, специфику задачи верификации;

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

- Классы формул, к которым применим метод или техника, п классы теорий, в рамках которых проводится доказательство.

Первую группу методов составляют универсальные методы [18. 20, 104], которые включают резолюцию [27, 36], обратный метод Маслова [26] и полные табличные методы [44, 103, 122]. Другие универсальные методы, основанные на том или ином исчислении и чисто дедуктивном выводе, не входят в эту группу, так как они не ориентированы на автоматическое доказательство. К досто-

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

Вторую группу методов составляют разрешающие процедуры для конкретных теорий, например для арифметики Пресбургера и ее расширений [35, 133, 134], теории списков [116, 121], арифметики сложения рациональных чисел [135], комбинации теорий с помощью равенств и дизъюнкций равенств [114, 115]. Достаточно полный обзор таких теорий можно найти в [34]. Они имеют довольно высокую эффективность, часто позволяют легко строить контрпримеры (например метод Шостака для арифметики Пресбургера). но класс таких теорий узок и не позволяет охватить проблемные области, к которым применяется верификация программ на практике.

Среди техник, применяемых в автоматическом доказательстве, можно выделить технику переписывания термов [11, 25, 28, 53, 84]. основанную на системах переписывания термов (СПТ), и технику сужения [69].

Техника переписывания термов [42, 78 — 81, 102] позволяет приспосабливать доказательство к конкретным проблемным областям. Для этого достаточно лишь модифицировать СПТ, лежащую в основе разрешающей проц^д^'ры. СПТ довольно эффективны, так как основаны на простом механизме сопоставления с образном

и не требуют разбора случаев. Ряд условий корректности, появляющихся при верификации программ, не требует для своего доказательства ничего, кроме применения некоторых лемм, аксиом и теорем, представимых в виде равенств. Доказательство таких условий корректности часто можно автоматизировать с помощью СПТ. Системы переписывания термов являются также хорошим аппаратом доказательства свойств алгебраических типов данных [2, 23], используемых в языках спецификаций. В то же время при верификации программ встречаются условия корректности, не позволяющие проводить доказательства по типу замены равных равными, лежащему в основе СПТ. К тому же при проведении доказательства часто требуется разбор случаев. И хотя были разработаны различные обобщения СПТ:

- условные СПТ [60, 64, 94, 112, 128, 146], допускающие применение правила переписывания при выполнении определенного условия,

- эквациональные СПТ [40, 46, 58, 82, 90 — 92,126, 145]. комбинирующие применение правил переписывания с выводом в экваци-ональных теориях,

- СПТ со встроенными разрешающими процедурами [13 — 16].

- СПТ для теорий, которые не являются квазиэквациональными, в частности, для логики первого порядка [96, 125],

- СПТ с разбором случаев [17],

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

Техника сужения представляет собой объединение переписывания и унификации. Эта техника проверки выполнимости формул исторически возникла как средство решения проблемы унифика-

ции в эквациональных теориях (Е'-унификации), была распространена на условные равенства [61, 62, 87, 95] и нашла применение как механизм, позволяющий объединять логические и функциональные языки [70, 74 —76, 110]. Разрешающие процедуры, основанные на сужении, также легко модифицируются при переходе от одной проблемной области к другой, как и процедуры, основанные на переписывании. Эта техника позволяет находить конкретные символические решения (унификаторы) и даже множество всех основных символических решений (наиболее общих унификаторов), если система переписывания, лежащая в ее основе, является полной (нете-ровой и конфлюентной). Унификация, используемая при сужении, позволяет моделировать такое мощное упрощение формул как замена переменных. В то же время перебор, возникающий при применении техники сужения, создает большое пространство поиска, что приводит к быстрому исчерпыванию скоростных и временных ресурсов машины. Еще одной сложностью, связанной с сужением, является более сложный механизм применения этой техники по сравнению с СПТ, требующий вычисления при каждом применении правила переписывания наиболее общего унификатора. Для решения этой проблемы разработано множество стратегий [65, 66] (нормальное сужение [67], базисное сужение [86], комбинация базисного и нормального сужения [120, 129], стратегия "самый внутренний" [70], ленивое сужение [144]), позволяющих уменьшить перебор, но эти стратегии не привязаны к конкретным проблемным областям и уменьшают перебор лишь незначительно. Другое направление, в котором ведутся исследования, является установление полноты сужения при более слабых ограничениях, накладываемых на СПТ. В этом направлении получены некоторые результаты для конфлю-ентных [86] и полуполных (semi-complete) [143] СПТ. К сожалению, ориентированность техники сужения в основном на разрешение

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

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

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

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

щается по сравнению с сужением, так как применяются не произвольные правила из некоторой СПТ как в технике сужения, а только конкретные выбранные подмножества СПТ — основы правил, входящих в СПФ. Но самое главное преимущество СПФ по сравнению с техникой сужения заключается в том, что они применяются к V- и 3-формулам, а не только к бескванторным равенствам. Более того, в качестве теорий, в рамках которых проводится доказательство, уже можно использовать теории с кванторами, а не только эквациональные или квазиэквациональные (с условными равенствами) теории. Это происходит за счет того, что условия корректности для правил переписывания формул кроме равенств и условных равенств включают также \/3-формулы. Само понятие корректности для правил переписывания формул также изменяется. Если для правил переписывания термов оно обычно означает сохранение эквивалентности бескванторных формул при переписывании относительно некоторой алгебры, то для правил переписывания формул понятие корректности означает сохранение эквивалентности замкнутых V- и 3- формул относительно некоторой алгебраической системы.

СПФ хорошо сочетаются с универсальными методами автоматического доказательства и разрешающими процедурами для конкретных теорий. Связь с универсальными методами проявляется на уровне доказательства достаточных условий корректности для СПФ. Эти условия образуют достаточно широкий класс квантор-ных формул, доказательство которых лучше всего проводить с помощью универсальных методов. СПФ предназначены прежде всего для использования в качестве упрощающих процедур, сохраняющих выполнимость (переписывании замкнутых 3-формул в эквивалентные замкнутые 3-формулы). Тогда чтобы получить на их основе разрешающие процедуры требуется комбинирование

СПФ с разрешающими процедурами для нормальных форм (формул, которые уже не могут быть переписаны).

Сохранение выполнимости и довольно мощный механизм переписывания формул делают СПФ перспективным средством в логическом выводе с удовлетворением ограничений (constraint deduction) [52, 97].

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

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

В рамках проекта СПЕКТР [30, 32, 118, 119] разработан и реализован модуль доказательства^ условий корректности, базирующийся на СПФ. Апробация осуществлялась для трех классов программ — программ редактирования текстов, сортировки массивов и сортировки последовательных файлов. Эксперименты показали, что комбинирования СПФ с разрешающими процедурами для арифметики Пресбургера и ее расширений, равенства, частичного порядка и равенства на мультимножествах оказалось достаточно, чтобы автоматически верифицировать достаточно широкий класс программ из этих проблемных областей. Это подтверждает практическую ценность результов работы.

Опишем структуру диссертации.

Первая глава посвящена теории СПФ. В §1 даны основы теории СПТ, включая условные СПТ, унификацию и сужение. В §'2 вводится понятие системы переписывания формул и рассматриваются ключевые свойства СПФ — нетеровость (отсутствие бесконечных цепочек переписываемых формул) и корректность (переписывание замкнутых V- и 3-формул в эквивалентные формулы). Сформулированы достаточные условия корректности СПФ, показана неразрешимость проблемы нетеровости и рассмотрена связь нетеро-вости СПФ с порядками упрощения. В §3 предложены специальные классы СПФ, завершающиеся относительно стратегии " любой самый внутренний". При этой стратегии СПФ применяется к самой внутренней позиции в формуле из всех позиций, к которым она применима. Выбор этих классов СПФ обоснован тем, что меру упрощения для таких систем нетрудно определить. Она задается элиминацией определенных функциональных символов (анализаторов). Другая причина рассмотрения таких систем заключается в том, что они полезны в алгебраических спецификациях типов данных, позволяя просачивать и элиминировать некоторые операции на типах данных, определяемых с помощью конструкторов.

Вторая глава посвящена методологии применения СПФ в автоматическом доказательстве. Для получения достаточно мощных разрешающих процедур необходимо комбинирование упрощающих процедур, основанных на СПФ, с базовыми разрешающими процедурами. В §1 описаны базовые разрешающие процедуры для теорий равенства, частичного порядка, арифметики Пресбургера и равенства мультимножеств. В §2 рассматриваются особенности применения СПФ в многосортных теориях. Вводится новый класс теорий сортов — теории сортов, определяемые обобщенными конструкторами, рассматривается связь этих теорий с корректностью СПФ, даются конкретные СПФ для булевского сорта. В

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

Третья глава посвящена методологии применения СПФ в верификации программ. В §1 дается метод Хоара верификации программ, кратко описывается система верификации СПЕКТР, основанная на этом методе, и приводится синтаксис языка аннотированных программ, используемого в примерах. В §2 СПФ используются в качестве средства преобразования структур данных языков программирования в сорта языков спецификаций на примере преобразования массивов и последовательных файлов в кортежи. В §3 описан модуль переписывания формул, основанный на СПФ. Рассматривается общая логическая структура модуля основные компоненты и связи между ними, приведены встроенные средства создания разрешающих процедур (тактик) — тактикалы, описаны результаты эксперимента по применению модуля для доказательства условий корректности, возникающих при верификации ряда программ редактирования текстов, сортировки массивов и файлов. Язык спецификаций, необходимый для описания аннотированных программ из данных классов, и конкретные тактики доказательства условий коррел.х*пости, основанные на СПФ, даются в §4. В качестве примеров выбраны программы копирования файла, линейного поиска, сортировки вставкой, быстрой сортировки и сортировки файлов естественным слиянием.

Основные результаты, включенные в диссертацию, отражены в публикациях [5 — 10].

Автор благодарит своего научного руководителя В.А. Непомнящего за всестороннюю поддержку и внимание к работе.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Ануреев, Игорь Сергеевич

Заключение

В работе получены следующие основные результаты.

1. Разработана новая техника автоматического доказательства, являющаяся обобщением как техники сужения, так и техники переписывания термов, — техника переписывания формул, базирующаяся на системах переписывания формул. Эта техника включает:

- новое понятие корректности — сохранение эквивалентности замкнутых V- и 3-формул при переписываниях;

- метод доказательства корректности (теорема корректности);

- методы проверки завершимости систем переписывания формул (униформные системы, системы элиминации анализаторов и их обобщение на аргументный статус, системы элиминации анализаторов с базой подстановок).

2. Предложена методология применения систем переписывания формул в автоматическом -доказательстве и верификации программ, включающая

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

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

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

3. В рамках системы верификации СПЕКТР реализован модуль переписывания формул, базирующийся на СПФ, и проведен программный эксперимент, который показал, что СПФ вместе с процедурами для конкретных разрешимых теорий обеспечивают автоматическую верификацию ряда программ редактирования текстов, сортировки массивов и файлов.

Список литературы диссертационного исследования кандидат физико-математических наук Ануреев, Игорь Сергеевич, 1998 год

Список литературы

[1] Абрамов С. А. Элементы анализа программ. — М.: Наука, 1986. — 128 с.

[2] Агафонов В.Н. Типы и абстракция данных в языках прокламирования (обзор) // Д«„;:пые в языках программирования. -М.: Мир, 1982. — С. 265—327.

[3] Агафонов В.Н. Спецификация программ: понятийные средства и их организация. — Новосибирск: Наука, 1987. — 240 с.

[4] Алагич С., Арбиб М. Построение корректных структурированных программ. — М.: Радио и связь, 1984. — 264 с.

[5] Ануреев И. С. Интегрированные правила переписывания термов и их применение в автоматической верификации программ // Проблемы спецификации и верификации параллельных систем. — Новосибирск, 1995. — С. 185—213.

[6] Ануреев И. С. Системы переписывания формул. — Новосибирск, 1997. — 22 с. — (Препр./РАН. Сиб. отд-ние. ИСИ; №40).

[7] Ануреев И.С. Упрощающие процедуры для типов данных, основанные на системах переписывания формул. — Новосибирск, 1998. — 43 с. — (Препр./РАН. Сиб. отд-ние. ИСИ; №53).

[8] Ануреев И.С. Теория систем переписывания формул. — Новосибирск, 1998. — 35 с. — (Препр./РАН. Сиб. отд-ние. ИСИ: №54).

[9] Ануреев И.С. Применение систем переписывания формул в автоматической верификации программ. — Новосибирск, 1998. — 47 с. — (Препр./РАН. Сиб. отд-ние. ИСИ; №55).

[10] Ануреев И. С. Системы переписывания формул и их применение в автоматической верификации программ. — ИНПРИМ. Тезисы докладов, часть V. — Новосибирск: Изд-во Института математики СО РАН, 1998. — С. 37.

[11] Бухбергер Б., Лоос Р. Упрощение алгебраических выражений // Компьютерная алгебра. Символьные и алгебраические вычисления. — М.: Мир. 1986. — С. 23—65.

[12] Вирт Н. Алгоримы и структуры данных. — М.: Мир, 1989. — 360 с.

[13] Воробьев С.Г. Переписывающие методы доказательства теорем в импликативных над базисными теориях // Всесоюз. конф. по прикладной логике: Тез. докл. — Новосибирск: Ин-т математики СО РАН СССР, 1985. — С. 39—42.

[14] Воробьев С.Г. О выразительной силе систем переписывания термов // Применение методов математической логики (Секция "Представление знаний и синтез программ"): Тез. докл. IV Всесоюз. конф. — Таллин: Ин-т кибернетики АН ЭССР. 1986. — С. 48—50.

[15] Воробьев С.Г. О применении условных систем подстановок термов в верификации программ // Программирование. 1986. — №4. — С. 3—14.

[16] Воробьев С.Г. О встраивании разрешимых фрагментов арифметики в системы переписывания термов // Методы трансляции и конструирования программ. — Новосибирск: ВЦ СО АН СССР, 1986.

[17] Воробьев С.Г. Системы условных редукций и их применение в проблемно-ориентированной верификации программ: Дис. канд. физ.-мат.наук:05.13.11. — Новосибирск, 1987. — 150 с.

[18] Воронков A.A., Дегтярев А.И. Автоматическое доказательство теорем I // Кибернетика. — 1986. — №3. — С. 27—33.

[19] Вульф В., Лондон Р., Шоу М. Введение в построение и верификацию программ на языке Альфард // Данные в языках программирования. — М.: Мир, 1982. — С. 123—153.

[20] Глушков В.М., Капитонова Ю.В., Летичевский A.A. Инструментальные средства проектирования программ обработки математических текстов // Кибернетика. — 1979. — №2. -С. 37—42.

[21] Грис Д. Наука программирования. — М.: Мир, 1984. — 416 с.

[22] Дейкстра Э. Дисциплина программирования. — М.: Мир, 1978. — 275 с.

[23] Замулин A.B. Типы данных в языках программирования и базах данных. — Новосибирск: Наука, 1987. — 150 с.

[24] Компьютерная алгебра. Символьные и алгебраические вычисления — М.: Мир, 1986. — 392 с.

[25] Кучеров Г.А. Системы подстановок термов. — Новосибирск. 1985. — 46 с. — (Препр./СО АН СССР. ВЦ; №601).

[26] Маслов С.Ю., Минц Т.Е. Теория поиска вывода и обратный метод // Математическая логика и автоматическое доказательство теорем. — М.: Наука, 1983. — С. 291—314.

[27] Маслов С.Ю. О стратегиях метода резолюций и клаш-метода // Математическая логика и автоматическое доказательство теорем. — М.: Наука, 1983. — С. 326—332.

[28] Массер Д. Спецификация абстрактных типов данных в системе AFFIRM // Требования и спецификации в разработке программ. — М.: Мир, 1984. — С. 199—222.

[29] Мендельсон Э. Введение в математическую логику. — М.: Наука, 1976. — 320 с.

[30] Непомнящий В.А. ВеригЬикация программ над массивами // Системная информатика. Вып.З. Программные и вычислительные системы: Методы и языки анализа. — Новосибирск: ВО Наука. Сибирская издательская фирма, 1993. — С. 68—98.

[31] Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. — М.: Радио и связь, 1988. — 256 с.

[32] Непомнящий В. А. Сулимов А. А. Верификация программ линейной алгебры в системе СПЕКТР // Кибернетика и системный анализ. — 1992. — №5. — С. 136—144.

[33] Непомнящий В. А. Сулимов А. А. Проблемно-ориентированные базы знаний и их применение в системе верификации программ СПЕКТР // Изв. РАН. Сер. Теория и системы управления. -1997. — №2. — С. 169—175.

[34] Рабин М.О. Разрешимые теории // Справочная книга по математической логике. — М.: Наука, 1982. — Т. 3. — С. 77—111.

[35] Семенов A.JI. Разрешающие алгоритмы для логических теорий // Кибернетика и вычислительная техника. — М.: Наука, 1986. — Т. 2. — С. 134—146.

[36] Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. — М.: Наука, 1983. — 360 с.

[37] Ющенко Е.Л., Касаткина И.В. Современные методы доказательства правильности iiporpaMM // Кибернетика, 1980. — №6. — С. 37—62.

[38] Apt K.R. Logic programming. Formal Models and Semantics // Handbook of Theor. Comput. Sci. — 1990. — Vol. B. — P. 495 574.

[39] Apt K.R. Ten years of Hoare's logic: a survey. Part I // ACM Trans. Progr. Lang. Syst. — 1981. — Vol. 3, — №4. — P. 431— 483.

[40] Bachmair L., Dershowitz N. Completion for rewriting modulo a congruence // Theor. Comput. Sci. —1989. — №67 (2-3). — P. 173—202.

[41] Bachmair L., Dershowitz N. Commutation, transformation and termination // Lect. Notes Comput. Sci. — 1986. — Vol. 230.

P. 5—20.

[42] Bachmair L., Ganzinger H. Rewrite-based equational theorem proving with selection and simplification // J. of Logic and Computation. — 1994. — №4(3). — P. 1—31.

[43] Bachmair L., Plaisted D.A. Associative path ordering // Lect. Notes Comput. Sci. — 1985. — Vol. 202. — P. 241—254.

[44] Beckert B., Hahnle R., Oel P., Sulzmann M. The tableau-based theorem prover 3TAP, version 4.0 // Lect. Notes Comput. Sci. 1996. — Vol. 1104. — P. 303—307.

[45] Bergstra J.A., Klop J.W. Conditional rewrite rules: confluence and termination // J. Comput. and Syst. Sci. — 1986. — №32 (3).

P. 323—363.

[46] Buchberger B. Basic features and development of the Critical-pair/Completion procedure // Lect. Notes Comput. Sci. — 1985. — Vol. 202. — P. 1—45.

[47] Burstall R.M., Goguen J.A. The semantics of CLEAR, a specification language // Lect. Notes Comput. Sci. — 1980. — Vol. 86.

— P. 292—332.

[48] Clarke E.M. Programming language constructs for which it is possible to obtain good Hoare axiom system //J. ACM. — 1979. — Vol. 26, №1. — P. 129—147.

[49] Comon H. Constraints in term algebras. An overview of constraint solving techniques // Lect. Notes Comput. Sci. — 1995. — Vol. 910. — P. 62—67.

[50] Dauchet M. Simulation of Turing machines by a left-linear rewrite rule // Lect. Notes Comput. Sci. — 1989. — Vol. 355. — P. 109— 120.

[51] De Champeaux D. About the Paterson-wegman linear unification algorithm //J. Comput. Syst. Sci. — 1986. — Vol. 32. — P. 79— 90.

[52] Comon H. Constraints in term algebras. An overview of constraint solving techniques // Lect. Notes Comput. Sci. — 1995. — Vol. 910. — P. 62—67.

[53] Dershowitz N. Computing with rewrite systems // Information and Control. — 1985. — Vol. 65. — P. 122—157.

[54] Dershowitz N. Ordering for term-rewriting systems // Proc. of the 20th Annual Symposi. on Foundations of Computer Science. San Juan, 1979. — P. 123—131.

[55] Dershowitz N. Termination // Lect. Notes Comput. Sci. — 1985.

— Vol. 202. — P. 180—224.

[56] Dershowitz N., Hoot C. Topics in termination // Lect. Notes Comput. Sci. — 1993. — Vol. 690. — P. 198—212.

[57] Dershowitz N., Jouannaud J.-P. Rewrite systems // Handbook of Theor. Comput. Sci. — 1990. — Vol. 6. — P. 243—320.

[58] Dershowitz N., Mitra S., Sivakumar G. Equation solving in conditional AC-theories // Lect. Notes Comput. Sci. — 1990. — Vol. 463. — P. 283—297.

[59] Dershowitz N., Sivakumar G. Solving goals in equational languages. // Lect. Notes Comput. Sci. — 1987. — Vol. 308. — P. 45—55.

[60] Dershowitz N., Plaisted D.A. Conditional rewriting // Software Eng.Notes. — 1985. — Vol. 10, №4. — P. 55—59.

[61] Dershowitz N., Plaisted D.A. Logic programming cum applicative programming // Proc. of the 2nd IEEE Symposi. on Logic Programming. — Boston, 1985. — P. 54—66.

[62] Dershowitz N., Plaisted D.A. Equational programming // Machine Intelligence. — 1987. — №11. — P. 21—56.

[63] Downey P.J., Sethi R., Tarjan R.E. Variations on the common subexpression problem //J. ACM. — 1980. — Vol. 27, №4. — P. 758—771.

[64] Drosten K. Towards executable specification using conditional axioms // Lect. Notes Comput. Sci. — 1984. — Vol. 166. — P. 85 96.

[65] Echahed R. On completeness of narrowing strategies // Theor. Comput. Sci. — 1990. №72. — P. 133—146.

[66] Echahed R. Uniform narrowing strategies // Lect. Notes. Comput. Sci. 1992. — №632. — P. 259—275.

[67] Fay M. First-order unification in equational theories // Proc. of the 4th Internati. Workshop on Automated Deduction. — Austin. 1979. — P. 161—167.

[68] Ferro A., Omodeo E.G., Schwartz J.T. Decision Procedures for some fragments of set theory // Lect. Notes Comput. Sci. — 1980.

— Vol. 87. — P. 88—96.

[69] Fribourg L. A narrowing,procedure for theories with constructors // Lect. Notes Comput. Sci. — 1984. — Vol. 170. — P. 259—281.

[70] Fribourg L. SLOG: A logic programming language interpreter based on clausal superposition and rewriting // Proc. of the 2nd IEEE Symposi. on Logic Programming. — Boston, 1985. — P. 172—184.

[71] Ganzinger H., Giegerich R. A note on termination in combinations of heterogeneous term rewriting systems // Bull. Europ. Association for Theor. Comput. Sci. — 1987. — №31. — P. 22—28.

[72] Gerhart S.L. An overview of AFFFIRM: a specification and verification system // Proc. IFIP Congress (Tokyo, Melbourne, 1980).

— Amsterdam: North-Holland, 1980. — P. 343—347.

[73] Gerhart S.L. Program verification in the 1980's // Proc. Conf. Computing in the 1980's. — Oregon, IEEE, 1978. — P. 80—98.

[74] Giovannetti E., Levi G., Moiso C., Palamidessi C. Kernel-LEAF: A logic plus functional language //J. Comput. and Syst. Sci. — 1991. — №42. — P. 139—185.

[75] Goguen J.A., Meseguer J. EQLOG: Equality,types and generic modules for logic programming // Logic Programming: Functions. Relations and Equations. — Englewood cliffs: Prentice Hall. 1986.

— P. 295—363.

[76] Hanus M. Compiling logic programs with equality // Lect. Notes Comput. Sci. — 1990. — №456. — P. 387—401.

[77] Holldobler S. Foundations of Equational Logic Programming // Lect. Notes Comput. Sci. — 1989. — Vol. 353. — P. 140—147.

[78] Hsiang J. Two results in term rewriting theorem proving // Lect. Notes Comput. Sci. — 1985. — Vol. 202. — P. 301—324.

[79] Hsiang J. Refutational theorem proving using term rewriting systems // Artif. Intell. — 1985. — Vol. 25, №2. — P. 255—300.

[80] Hsiang J., Dershowitz N. Rewrite methods for clausal and non-clausal theorem proving / / Lect. Notes Comput. Sci. — 1983. — Vol. 154. — P. 331—346.

[81] Hsiang J., Kirchner H., Lescanne P., Rusinowitch M. Automated theorem proving in the presence of equalities // J. Automat. Re-seach. — 1992. — Vol. 14. — P.71—100.

[82] Huet G., Hullot J.M. Proofs by induction in equational theories with constructors //J. Comput. System Sci. — 1982. — Vol. 25, No 2. — P. 239—266.

[83] Huet G., lankford D.S. On the uniform halting problem for term rewriting systems. — Paris, 1978. — (INRIA Lab.; Rep. №283).

[84] Huet G., Oppen D.C. Equation and rewrite rules. A survey // Formal language theory: Perspectives and Open Problems. — New York: Acad. Press, 1980. — P. 349—406.

[85] Huet G. Confluent reductions: abstract properties and applications to term rewriting systems //J. ACM. — 1980. — Vol. 27. №4. — P. 797—821.

[86] Hullot J.M. Canonical forms and unification // Lect. Notes Comput. Sci. — Vol. 87. — 1980. — P. 318—334.

[87] Hufimann H. Unification in conditional-equational theories // Lect. Notes Comput. Sci. — Vol. 204. — 1985. — P. 543—553.

[88] Igarashi S., London R.L., Luckham D.C. Automatic program verification I: a logical basis and its implementation // Acta Informática. — 1975. — Vol. 4, №2. — P. 145—182.

[89] Jantzen M. Confluent string rewriting and congruences // Europ. Association for Theor. Comput. Sci., Monographs on Theor. Com-put. Sci. — 1988. — Vol. 14. — P. .

[90] Jouannaud J.P. Confluent and coherent equational term rewriting systems: applications to proofs in abstract data types // Lect. Notes Comput. Sci. — 1983. — Vol. 159. — P. 269—283.

[91] Jouannaud J.P., Kirchner H. Completion of a set of rules modulo a set of equations // SIAM J. of Computing. — 1986. — №15 (4).

— P. 1155—1194.

[92] Jouannaud J.P., March e C. Copletion modulo associativity, com-mutativity and identity (ACI) // Lect. Notes Comput. Sci. — 1990.

— Vol. 429. — P. 111—120.

[93] Jouannaud J.P., Waldmann B. Reductive conditional term rewriting systems // Proc. of the 3rd IFIP Working Conference on Formal Description of Programming Concepts. — Ebberup, 1986. — P. 223—244.

[94] Kaplan S. Conditional rewrite rules // Theor. Comput. Sci. —

1984. — Vol. 33, №2-3. — P. 175—193.

[95] Kaplan S. Simplifying conditional term rewriting systems: unification, termination and confluence //J. Symb. Comput. — 1987.

— №4(3). — P. 295—334.

[96] Kapur D., Narendran P. An equational approach to theorem proving in first order predicate calculus // Software Eng. Notes.

1985. — Vol. 10, №4. — P. 63—66.

[97] Kirchner H. On the use of constraints in automated deduction // Lect. Notes Comput. Sci. — 1995. — Vol. 910. — P. 128—146.

[98] Klop J.W. Term rewriting systems // Handbook Logic Comp. Sci.

— 1993. — Vol. 2. — P. 1—116.

[99] Klop J.W. Combinatory reduction systems // Mathematical Centre Tracts. CWI, Amsterdam, 1980.

[100] Kruskal J.B. Well-quasi-ordering, the tree theorem and Vaz-sonyi's conjecture // Trans. AMS. — 1960. — №95. — P. 210—225.

[101] Lankford D.S. Some approaches to equality for computational logic: a survey and assessment. — Univ. of Texas, 1977. — (Rep. ATP-36).

[102] Lescanne P. Term rewriting systems and algebra // Lect. Notes Comput. Sci. — 1984. — Vol. 170. — P. 166—174.

[103] Letz R., Schumann J.. Bayerl S., Bidel W. SETHEO: A highperformance theorem prover //J. Automat. Reasoning. — 1992. — Vol. 8, №2. — P. 183—212.

[104] Loweland D.W. Automated theorem proving: a quarter century review // Contemporary Mathematics. — 1984. — Vol. 29. — P. 1—42.

[105] Manna Z., Waldinger R. The logic of computer programming // IEEE Trans. Software Eng. — 1978. — Vol. SE-4, №3. — P. 199— 229.

[106] Martelli A., Montanari U. An efficient unification algorithm // ACM Trans. Prog. Lang, and Syst. — 1982. — Vol. 4, №2. — P. 258—282.

[107] Mateti P. A decision procedure for the correctness of a class of programs // J. ACM. — 1981. — Vol. 28, №2. — P. 215—232.

[108] Meinke K., Tucker J.V. Universal algebra. // Handbook Logic Comp. Sci. — 1992. — Vol. 1. — P. .

[109] Middeldorp A. A sufficient condition for the termination of the direct sum of term rewriting systems // Proc. of. the 4th IEEE

Symposi. on Logic in Comput. Sci. — Pacific Grove, 1989. — P. 396—401.

[110] Moreno-Navarro J.J., Rodriguez-Artalejo M. BABEL: A functional and logic programming language based on constructor discipline and narrowing // Lect. Notes Comput. Sci. — 1989. — Vol. 343. — P. 223—232.

[111] Moriconi M., Schwartz R.L. Automatic construction of verification condition generators from Hoare's logics // Lect. Notes Comput. Sci. — 1981. — Vol. 115. — P. 363—377.

[112] Navarro M., Orejas F. On the equivalence of hierarchical and non-hierarchical rewriting in conditional term rewriting systems // Lect. Notes Comput. Sci. — 1984. — Vol. 174. — P. 74—85.

[113] Nederpelt R.P. Strong normalization for a typed lambda calculus with lambda structured types. PhD thesis, Technische HogeschooL Eindhoven, The Netherlands, 1973.

[114] Nelson G. Combining satisfiability procedures by equality sharing // Contemporary Mathematics. — 1984. — Vol. 29. — P. 201— 211.

[115] Nelson G., Oppen D.C. Simplification by cooperating decision procedures // ACM Trans. Progr. Lang. Syst. — 1979. — Vol. 1. №2. — P. 245—257.

[116] Nelson G., Oppen D.C. Fast desition procedures based on congruence closure //J. ACM. . 1980. — Vol. 27, №2. — P. 356—364.

[117] Nepomniaschy V.A. On a symbolic method of verification for definite iteration over data structures // Joint Bulletin of the Institute of Informatics Systems and Computer Center. — 1998. — №5. — P. 1—22.

[118] Nepomniaschy V.A., Sulimov A.A. Problem-Oriented Means of Program Specification and Verification in Project SPECTRUM // Lect. Notes Comput. Sci. — 1993. — Vol. 722. — P. 374—378.

[119] Nepomniaschy V.A., Sulimov A.A. Towards Automatic Program Verification: Problem-Oriented Knowledge Bases // Specification, verification and net models of concurrent systems. — Novosibirsk, 1994. — P. 138—150

[120] Nutt W., Rety P., Smolka G. Basic narrowing revisited //J. Symb. Comput. — 1989. — №7. — P. 295—317.

[121] Oppen D.C. Reasoning about recursively defined data structures // J. ACM. — 1980. — Vol. 27, №3. — P. 403—411.

[122] Oppacher F., Suen E. HARP: A tableau-based theorem prover // J. Automat. Reasoning. — 1988. — Vol. 4. — P. 69—100.

[123] Owre S., Rushby J., Shankar N. PVS: A prototype verification system // Lect. Notes Art. Intell. — 1992. — Vol. 607. — P. 748752.

[124] Oyamaguchi M. The Church-Rosser property for ground term rewriting systems is decidable // Theor. Comput. Sci. — 1987. — №49 (1). — P. 43-79.

[125] Paul E. Equational methods in first order predicate calculus // J. Symb. Comput. — 1985. — №1. — P. 7—29.

[126] Peterson G.E., Stickel M.E. Complete sets of reductions for some equational theories //J. ACM. — 1981. — Vol. 28, No 2. - P. 233—264.

[127] Plaisted D.A. A recursively defined ordering for proving termination of term rewriting systems. — University of Illinois, 1978. — (Dept. of Computer Science; Rep. UIUCDCS-R-78-943).

[128] Remy J.-L., Zhang H. REVEUR 4: A system for validating conditional algebraic specifications of abstract data types // Proc. 6th Europ. Conf. on Artificial Intell. (ECAI-84). — , 1984. — P.563-572.

[129] Rety P. Improving basic narrowing techniques // Lect. Notes Comput. Sci. — 1987. — Vol. 256. — P. 228—241.

[130] Rusinowitch M. On termination of the direct sum of term rewriting systems. // Information Processing Letters. — 1987. — №26.

— P. 65—70.

[131] Rusinowitch M. Path of subterms ordering and recursive decomposition ordering revisited // J. of Symb. Comput. — 1987. — .№3.

— P. 117—131.

[132] Schwartz J.T. A survey of program proof technology. — New York Univ., 1978. — (Dep. Comput. Sci.; Rep. №001).

[133] Shostak R.E. On the SUP-INF method for proving Presburger formulas // J. ACM. — 1977. — Vol. 24, №4. — P. 529—543.

[134] Shostak R.E. A practical decision procedure for arithmetic with function symbols // J. ACM. — 1979. — Vol. 26, №2. — P. 351— 360.

[135] Shostak R.E. Deciding linear inequalitities by computing loop residues // J. ACM. — 1981. — Vol. 28, №4. — P. 769—779.

[136] Shostak R.E., Schwartz R., Melliar-Smith P.M. STP: A mechanized logic for specification and verification // Lect. Notes Corn-put. Sci. — 1984. — Vol. 170. — P. 1—42.

[137] Siekmann J. Universal unification // Lect. Notes Comput. Sci. — 1984. — Vol. 170. — P. 1—42.

[138] Staples J. Church-Rosser theorems for replacement systems // Algebra and Logic, Lect. Notes in Math. — 1975. — Vol. 450. — R 291—307.

[139] Steinbach J. Simplification ordering: history of results // Fundamenta Informaticae. — 1995. — Vol. 24, №1. — P.47—87.

[140] Suzuki N., Jefferson D. Verification decidability of Presburger array programs // J. ACM. — 1980. — Vol. 27, №1. — P. 191— 205.

[141] Toyama Y. On the Church-Rosser property for the direct sum of term rewriting systems //J. ACM. — 1987. — №34 (1). — P. 128—143.

[142] Toyama Y., Klop J.W., Barendregt H.P. Termination for the direct sum of left-linear term rewriting systems // Lect. Notes Com-put. Sci. — 1989. — Vol. 355. — P. 477—491.

[143] Yamamoto A. Completeness of extended unification based on basic narrowing // Proc. of the 7th Logic Programming Conference.

— Jerusalem, 1988. — P. 1—10.

[144] You Y.H. Enumerating outer narrowing derivations for constructor based term rewritm0* _ystems //J. Symb. Comput. — 1989.

— №7. — P. 319—343.

[145] Zhang H., Kapur D. Unnecessary inferences in associative-commutative completion procedures // Mathe. Systems Theory.

— 1990. — №23. — P. 175—206.

[146] Zhang H., Remy J.-L. Contextual rewriting // Lect. Notes Comput. Sci. — Vol. 202. — P. 46—62.