Читать онлайн «Кибернетический сборник. Новая серия. Выпуск 25»

SZ ШЯЯ МИНсЮЗЭ ИИМЭЗЬИ13Нс139ИМ Кибернетический сборник НОВАЯ СЕРИЯ ВЫПУСК 25 Сборник статей Перевод с английского ПОД РЕДАКЦИЕЙ О. Б. ЛУПАНОВА и О. М. КАСНМ-ЗАДЕ МОСКВА «МИР» 1988 ББК 32. 81 К38 УДК 519. 95 Кибернетический сборник. Новая серия. Вып. 25. К38 Сб. статей 1983—1985 гг. : Пер. с англ. —М. : Мир, 1988. — 237 с. ,ил. ISBN 5-03-000999-Х В данном выпуске известной серии содержатся оригинальные и обзорные работы известных зарубежных ученых по актуальным проблемам теоретической кибернетики и ее приложениям. Автоматическому доказательству теорем посвящена статья Же Сяна (США), в статье Т. Феннера и А. Фриза (США) обсуждаются вопросы сложности и теории графов. Большой интерес представляют две статьи Ло Чжукая (КНР) по проблеме полноты в многозначной логике, статья Т. Хеллесета (Норвегия) по теории кодирования, а также работа С. Ёкои и др. (Япония) по новым методам распознавания цифровых изображений. Включены также обзоры советских авторов современных методов проверки простоты чисел и современного состояния в области алгоритмов матричного умножения. Сначала рассматривается пропозициональное исчисление и вводится каноническая переписывающая система для булевой алгебры. Эта система позволяет преобразовать исчисление предикатов первого порядка в некоторую форму эквациональной логики и разработать для теорий- первого порядка несколько полных стратегий (работающих как с дизъюнктами, так и с формулами более общего вида), основанных на процедуре пополнения Кнута — Бендикса. Что более важно, наши стратегии могут единообразно и эффективно работать с логикой Предикатов и «встроенными» (эквациональными) теориями. Мы описываем также реализацию этих стратегий и сравниваем их с некоторыми другими методами доказательства теорем первого порядка. 0. СТРУКТУРА СТАТЬИ Статья состоит из пяти разделов. В разд. 1 дается краткое изложение основных понятий метода переписывающих правил. В разд. 2 приводится каноническая переписывающая система для булевой алгебры. Эта система используется в разд. 3 как основа для разработки нескольких полных стратегий доказательства теорем в исчислении предикатов первого порядка. В разд. 4 данные стратегии расширяются на более богатые теории— логику первого порядка с встроенными эквациональными аксиомами. Реализация этих методов и результаты экспериментов обсуждаются в разд. 5. 1. ВВЕДЕНИЕ Переписывающая система для термов (term-rewriting system) для эквациональной теории Е есть конечное множество переписывающих правил /? = {//->г/}"ив1> такое, что {/i = r/}"el и Е эквивалентны (т.