Препринты Института систем информатики СО РАН 1998 г.

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

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

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

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

Универсальные методы решения задач изучаются в рамках научной дисциплины “искусственный интеллект”. Настоящая работа посвящена описанию недоопределенных моделей как аппарата для решения задач удовлетворения ограничений. Такие задачи возникают во многих областях науки и техники. Использование метода распространения ограничений в недоопределенных моделях позволяет оценивать множество всех решений такой задачи. В статье даются обоснования недоопределенных моделей. Предлагается понятие недоопределенного расширения многосортной модели, и обсуждаются различные типы таких расширений. Определяются денотационная и операционная семантики распространения ограничений в недоопределенных моделях и доказывается их эквивалентность.