Леммой называется любая аксиома вида . конкретных значений переменных х. Правило редукции для лемм выглядит следующим образом. В этом случае процедура у имеет вид. доказательства, которые не завершены, но их можно эффективно раскручивать до полного доказательства. Кроме обычных правил нормализации выводов в системе Гоуда реализовано еще правило подрезки доказательств, которое было предложено Правицем . Перейдем к системе Манны — Уолдингера . Метод поиска вывода в ней основан на тех же идеях, что и метод матричных редукций . Чтобы избежать неконструктивности, присущей этим методам, расщепления формулы берутся по разрешимым подформулам. Пусть из формул А. Тогда вначале составляется таблица следующего вида. Посылки Цель Результат В . Если в качестве аксиом использовать не только формулы Харропа, то нормализованный вывод формулы . Если, например, в В. , Ап В. цель совпадает с одной из посылок, или равна И, то ищется вывод для других строк. Когда вывод построен для всех строк, то, что стоит в графе . Методы конструктивного вывода, но для подмножества исчисления высказываний используются в планировщике системы ПРИЗ с входным языком УТОПИСТ . Если в случае использования семантик типа реализуемости реализация формулы хранит информацию, достаточную для ее обоснования, и вся эта информация извлекается из доказательства, то в системе ПРИЗ из доказательства извлекается только часть информации, а другая часть задается явно в виде более или менее обычной программы. Аксиомы, с которыми работает планировщик системы, являются формулами исчисления высказываний вида В или вида А. Вместе с каждой такой формулой задается ее реализация, которая в случае формулы А. Для используемого в ПРИЗе класса формул существуют очень эффективные алгоритмы поиска вывода . , ап, соответствующих Ль . Воронков ские аспекты использования формул указанного вида и их обобщений в синтезе программ рассматриваются в . Отметим, что работа планировщика скрыта от пользователя, которому надо только уметь описывать задачу на языке УТОПИСТ, а перевод такого описания в формулы, поиск вывода и синтез программы по готовому выводу осуществляются автоматически. ПРИЗ — одна из самых ранних систем логического программирования, хотя ее логический смысл в терминах исчисления высказываний был выявлен позднее. Плодотворная идея, воплощенная в системе ПРИЗ, получила развитие в ряде других отечественных систем автоматического синтеза программ. Система СПОРА с входным языком ДЕКАРТ . Специфика этого множества такова, что вместо обычного алгоритма обратной волны . ПРИЗ появился как подход к автоматизации решения некоторого класса задач, в которых важную роль играют описания связей между переменными . Еще одна реализованная отечественная система автоматического синтеза программ СИНТЕЗ . Синтез логических программ из конструктивных доказательств рассматривается в . У этого подхода по сравнению с традиционным подходом к извлечению программ из конструктивных доказательств имеются и преимущества и недостатки. Преимущества заключаются в том, что семантику для извлечения программ из доказательств можно объединить с теоретико. Вследствие этого можно писать смешанные программы, которые частично состоят из конструктивных доказательств, а частично — из хорновских дизъюнктов. Недостатки этого подхода вытекают из того, что для извлечения из доказательства эффективных программ скорее подходят языки функционального программирования. Для извлечения из доказательств программ. Более подробно с проблематикой дедуктивного синтеза программ можно познакомиться по работам . Типы и абстракция данных в языках программирования . : Данные в языках программирования. Языки и средства спецификации программ . : Требования и спецификации в разработке программ. Язык Декарт — входной язык системы СПОРА. : Прикладная информатика, вып. : Финансы и статистика, . ПРОЛОГ — язык логического программирования. О сокращении перебора при синтаксическом анализе. Схемы для функций и отношений. : Исследования по формализованным языкам и некласснческим логикам. Схемы на клубных системах и вегетативная машина. Семантика параметрических конструкций в логическом программировании. Пролог — основные идеи и конструкции. Управление памятью в реализациях Пролога. Система ПРИЗ и исчисление высказываний. О применении условных систем подстановок термов в верификации программ. Один метод поиска доказательства. Способы выполнения программ в . Логические программы и их синтез. Новосибирск, Препринт Института математики СО АН СССР, . сибирск, Препринт Института математики СО АН СССР, . Конструктивная истинность и конструктивные исчисления. Вопросы теории и практики. Синтез логических программ. Логический вывод в системе автоматизации доказательств. : Математические основы систем искусственного интеллекта, Киев, . Методы управления равенством в машинном доказательстве теорем. Методы обращения с равенством для хорновских множеств. : Методы алгоритмизации и реализации процессов решения интеллектуальных задач, Киев, . : Трансляция и оптимизация программ, Новосибирск. — Известия АН СССР. ЯРешение в линейное время алгоритмических проблем, связанных с синтезом ациклических программ. Вычислительные модели с разделяемыми подзадачами. Практическое использование Пролога, см. Смешанные вычисления в классе рекурсивных схем программ. : Методы математической логики в проблемах искусственного интеллекта и систематическое программирование. Динамическая логика над допустимыми множествами. Исчисление функциональных и неявных зависимостей. : Сложностные проблемы математической логики. Квазиполиномиальные алгоритмы распознавания выполнимости и выводимости пропозициональных формул. Спецификация численного интегрирования на языке логических программ. : Радио и связь, . Реляционный язык программирования и принципы его реализации на последовательной ЭВМ. Программирование на языке Пролог. К толкованию интуиционистской логики. Мобильная реализация языка программирования Микро.