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

I . и . '

I

и

на правах рукописи ЧАГРОВ Александр Васильевич

МОДЕЛИРОВАНИЕ ВЫЧИСЛИТЕЛЬНЫХ ПРОЦЕССОВ

СРЕДСТВАМИ ПРОПОЗИЦИОНАЛЬНЫХ логик

Специальности: 05.13.17 — Теоретические основы информатики, 01.01.06 — Математическая логика, алгебра и теория чисел

АВТОРЕФЕРАТ диссертации на соискание учёной степени доктора физико-математических наук

Москва 1998

Работа выполнена в Институте проблем передачи информации РАН.

Официальные оппоненты:

академик РАН, доктор физ.-мат. наук, профессор Ю.И.Журавлев доктор физ.-мат. наук, профессор М.А.Тайцлин доктор физ.-мат. наук, профессор Е.М.Вениаминов

Ведущая организация:

Институт прикладной математики РАН

Защита состоится "_"_1998 г. в 11 часов на заседании диссертационного совета Д 003.29.01 при Институте проблем передачи информации РАН по адресу: 101447, Москва, Б.Каретный пер., 19,

С диссертацией можно ознакомиться в библиотеке ИПГШ РАН. Автореферат разослан "_ 1 " 1998 г.

Учёный секретарь диссертационного совета

доктор тех. наук, профессор С.Н.Степанов

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы исследования В 70—80® годы было досрочно подтверждено предвидение создателя языка лисп Дж.Маккарти, высказанное им в 1967 году: ««Разумно ожидать, что связи между вычислительной техникой и математической логикой окажутся столь же плодотворными в следующем столетии, какими были связи между математическим анализом и физикой в столетии предыдущем»». Оказалось, что в плодотворности этих связей можно убедиться уже в наши дни1. Методы математической логики позволили осуществить новые подходы к созданию вычислительных средств, баз данных, экспертных систем, языков программирования, синтезу и верификации программ и т.п. При этом действенной оказалась и обратная связь: возникли новые разделы математической логики, оказались по-новому расставленными акценты в ряде её традиционных разделов. Практически в каждом справочном пособии и многих монографиях по информатике или искусственному интеллекту математическая логика выступает и в качестве языка обсуждения предмета, и в качестве необходимой компоненты представления результатов, и в качестве одного из инструментов для

предисловии редакторов сборника переводов [Математическая логика в программировании. (Ред.: М.В.Захарьящев, Ю.И.Янов.) М., Наука, 1991.) сказано, например: ««Чтобы представить себе, хотя бы в общих чертах, те направления, в которых развивается современная вычислительная наука, полезно взглянуть на названия сборников широко известной серии Lecture Notes in Computer Science, выпускаемой западногерманским издательством Spimgei-Verlag и содержащей материалы многих международных конференций по информатике. ... чуть ли не на каждой пятой обложке можно увидеть термины ««логический вывод»», ««логическое программирование»», ««компьютерная логика»», ««логики программ»» и т.д. »». Ещё раньше плодотворность применения средств математической логики в программировании была блестяще продемонстрирована в [E.W.DlJKSTRA. A Discipline of Programming // Prentice-Hall, Inc., Englewood Cliffs, N.J., 1976. (Русский пер.: Э.ДейКСТРА. Дисциплина программирования. М., Мир, 1978.)].

их получения2. Сейчас происходит переосмысление всего здания логики с учетом этой новой реальности: те её части, которые до того считались неклассическими и представляли собой нечто экзотическое, становятся едва ли не главными объектами исследований и приложений3. При этом особый интерес представляют логические системы, имеющие реляционное истолкование (в частности, в форме семантики): программные и динамические логики, модальные и многомодальные (особенно временные), интуиционистская4 и близкие к ней логики.

2См., например, [S.Abramsky, D.Gabbay, T.Mainbaum, eds. Handbook of Logic in Computer Science, Oxford, Clarendon Press, 1992.], [Dov M-Gabbay, C.J.hogger, J.A.ROBINSON. Handbook of Logic in Artifical Intelligence and Logic Programming, Oxford, Clarendon Press; Vol. 1: Logical Foundations, 1993, 518 pp.; Vol. 2: Deduction Methodologies, 1993, 518 pp.; Vol. 3: Nonmonotonic Reasoning and Uncertain reasoning, 1994, 529 pp.), [R.GOLDBLATT. Axiomatizing the Logic of Computer Programming. Berlin, Springer Verlag, 1982.], [D.Gabbay, I.hodklnson & M.Reynolds. Temporal Logic: Mathematical Foundations and Computational Aspects, Oxford, Clarendon Press, 1993.], [J.A.F.K. van benthem. Language in Action. Categories, Lambdas, and Dynamic logic. Amsterdam, North-Holland, 1991.].

3 Авторы [А.л.семёнов, В.А.Успенский. Математическая логика в вычислительных науках и вычислительной практике // Вестник АН СССР. 1986. N 7. С. 93-103.] говорят по этому поводу: ««С точки зрения названных задач перспективной кажется и разработка математических исчислений так называемой модальной логики, оперирующей, наряду с традиционными для классической логики оценками ««истинно»»» ««ложно»», также и такими оценками, как ««возможно»», ««необходимо»», ««правдоподобно»», ««произойдёт в будущем»» и т.д.»».

4Интуиционистская логика оказалась пригодной для описания свойств вычислений даже в тех случаях, когда логики на классической основе не давали непосредственной возможности для их использования, например: синтеза программ [Б.б.волож, М.б.МаЦКИН, Г.Е.Минц, Э.Х.Тыугу. Система ПРИЗ и исчисление высказываний // Кибернетика. 1982. N 6. С. 63-70.], [Г.Е.Минц, Э.Х.ТЫУГУ. Структурный синтез и неклассические логики // Тезисы докл. III Всесоюзной конференции ««Применение методов математической логики»». Таллин, 1983, с. 52-60.], для описания альтернирующих вычислений [27], моделирования немонотонных рассуждений [M.R.B.Clarke,

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

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

D.M.GABBAY. An intuitionistic basis for nonmonotonic reasoning. // Non-standard logics for automated reasoning, P.Smets, E.H.Mandami, D.Dubois, and H.Prade, eds., Academic Press, 1988, p. 164-174.].

5Рост значения модальной логики для информатики можно охарактеризовать таким фактом. Авторы монографии [A.ThaySE, P.GribomoNT, G.LOUIS, D.Snyers, P.Wodon, P.Gochet, E.Gregoire, E.Sanchez, Ph.Delsarte. Approche logique de l'intelligence artificielle. 1. De la logique classique à la programmation logique. Bordas, Paris, 1988. (Русский пер.: А.Тей, П.грибомон, Ж.ЛУИ И ДР. Логический подход к искусственному интеллекту. От классической логики к логическому программированию. М., Мир, 1990.)] отвели модальной логике в первом томе своего сочинения около 5% объёма текста, а второй том снабдили подзаголовком ««От модальной логики к логике баз данных»».

конкретных алгоритмов, которые в определённых случаях можно применять для решения прикладных задач, а ««отрицательный»» — ввиду того, что при доказательстве неразрешимости как органическую часть приходится использовать явное представление алгоритма в исчислении и, тем самым, разрабатывать выразительные возможности языка пропозициональных логик, таким образом расширять область их приложений6.

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

• представление вычислений средствами логического следования:

— в виде выводов в исчислениях;

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

— в виде допустимых в данной логике правил вывода; их наличие может существенно ускорить алгоритмы, распознающие принадлежность формул этой логике;

еКроме того, стоит иметь в виду и другой очевидный аспект ««отрицательных»» результатов, см. [А.Л.семёнов, В.а.успенский. Математическая логика в вычислительных науках и вычислительной практике // Вестник АН СССР. 1986. N 7. С. 93-103.]: ««Понимание, что в принципе невозможно сделать что-то, имеет для программирования не меньшее значение, чем для техники невозможность нарушить второе начало термодинамики или для физики невозможность превысить скорость света»».

в алгоритмическое описание свойств реляционных структур средствами пропозициональных языков:

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

— выяснение возможности переопределения реляционных свойств модальных, интуиционистских пропозициональных формул

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

• алгоритмическое описание свойств логик:

— выяснение по аксиоматизации логики ее семантических свойств, таких как:

* финитная аппроксимируемость, то есть возможность ограничения класса адекватных для логики структур конечными;

* реляционная полнота, то есть точность соответствия логики и класса моделирующих её реляционных структур;

* табличность логики, то есть её адекватность по отношению к одной конечной реляционной структуре;

— выяснение по аксиоматизации логики ее внутренних свойств, таких как7:

* непротиворечивость, то есть нетривиальность логики для дальнейших приложений;

7 Здесь указываются лишь центральные в некотором смысле свойства.

* разрешимость самой логики, разрешимость проблем допустимости в ней различных правил вывода;

* дизъюнктивное свойство, являющееся методологической основой построения большинства алгоритмов, синтезирующих программы по доказательству их существования; и близкие к нему свойства (полнота по Холдсну, полнота по Максимовой);

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

Целью работы являются:

• изучение феномена алгоритмической разрешимости/неразрешимости пропозициональных логик; в частности, выяснение границ применимости известных критериев разрешимости, например, критерия Харропа;

• создание простых в некотором смысле (удобных для приложений, экономных по числу переменных, используемых в соответствующей аксиоматике) неразрешимых исчислений;

• решение известных проблем, связанных с правилами вывода (в частности, всякая ли разрешимая логика имеет разрешимую проблему допустимости правил вывода) и с вариантами семантического следования (например, следования на конечных реляционных структурах);

• выяснение возможностей алгоритмического описания свойств логик (точнее, исчислений, ввиду известной теоремы А.В.Кузнецова об алгоритмической неразрешимости нетривиальных свойств рекурсивно задаваемых логик), то есть обоснование разрешимости

или неразрешимости интересующего нас по каким-либо причинам свойства логик.

Методы исследования Основные методы исследования — семантические методы теории модальных и суперинтуиционистских логик, методы теории моделей классической логики первого порядка, методы теории алгоритмов.

Научная новизна В диссертации получены следующие основные новые результаты:

• Построены примеры неразрешимых логик, задаваемых разрешимыми классами конечных шкал (алгебр, моделей); обосновано существование неразрешимых рекурсивно аксиоматизируемых финитно аппроксимируемых логик; показано, что не все логики можно аппроксимировать рекурсивными алгебрами.

• В следующей таблице

Число переменных в

Класс неразрешимых отделяемых

логик исчислениях формулах

ЕхИпЛ < 4 = 2

ЫЕх184 < з = 1

Ех1Б4 <3 — 1

ИЕх^СЬ = 1 = 1

Ех1СЬ = 1 = 1

Ех18 = 1 = 1

ГТЕхЖ4 = 1 = 0

ЕхЖ4 = 1 = 0

приведены обнаруженные в диссертации факты о существовании в рассматриваемых классах логик8 неразрешимых исчислений с малым числом переменных: первая строка, например, означает, что существует неразрешимое суперинтуиционистское исчисление, аксиомы которого используют 4 переменные, а в формулах, для которых неразрешима проблема выводимости в нем, используются 2 переменные; знак — около числа означает, что оценка числа переменных не понижаема, а < — вопрос о понижении числа переменных открыт.

• Предложено понятие разрешимой/неразрешимой в данном классе логик формулы, которое является двойственным понятию разрешимой/неразрешимой логики, и найдены простые (по числу переменных, используемым связкам, длине) для рассматриваемых классов логик примеры неразрешимых формул.

• Построена разрешимая модальная логика с неразрешимой проблемой допустимости правил вывода, что обосновывает нетривиальность задачи доказательства разрешимости проблемы допустимости правил вывода: положительное решение этой последней задачи было получено В.В.Рыбаховым для многих конкретных модальных и суперинтуиционистских логик.

• Доказана неразрешимость семантического следования на конечных шкалах Крипке в различных вариантах (локальном, глобальном) и в разных классах шкал (СЬ-шкалы, 1п1-шкалы и др.). Получена также неразрешимость проблемы первопорядко-вой определимости модальных формул на классе конечных шкал9.

'Здесь и далее используются стандартизированные в [62] обозначения: (К)Ех1Ь — класс (нормальных) расширений логики Ь; так, Ех^!^ обозначает класс су-перинтуинионистскгос логик, КЕхкЭ4 — класс нормальных расширений модальной логики в4.

'Результат получек совместно с Л.А.Чагровой; см. сноску на странице 16.

в Обоснована разрешимость некоторых свойств логик в некоторых классах —- в частности, свойство табличности и непротиворечивости расширений GL, а для значительного количества стандартных свойств логик, таких как разрешимость, финитная аппроксимируемость, полнота, интерполяционное и дизъюнктивное свойства и т.д., доказана алгоритмическая неразрешимость практически во всех рассматриваемых классах логик, кроме того, установлена граница разрешимости/неразрешимости таких свойств, как непротиворечивость и полнота по Холдену.

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

Апробация По результатам диссертации делались доклады на Всесоюзных конференциях по математической логике (Тбилиси, 1982; Новосибирск, 1984; Москва, 1986; Ленинград, 1988; Алма-Ата, 1990, приглашённый доклад), на Всесоюзных алгебраических конференциях (Кишинёв, 1985, Львов, 1987), на IX Всесоюзном совещании по логике, методологии и философии науки (Харьков, 1986), на Международных конгрессах по логике, методологии и философии науки (Москва, 1987; Italy, 1995), на X Всесоюзной конференции по логике, методологии и философии науки (Минск, 1990), на II Всесоюзной конференции по

прикладной логике (Новосибирск, 1988), на Международной конференции по алгебре (Новосибирск, 1989), на Логическом Коллоквиуме Европейской Ассоциации Символической логики (ASL Logic Colloquium 'Berlin 89'; The 1992 Europian Summer Meeting of the ASL, 1992; Logic Colloquium'94,1994), на логических конференциях в Болгарии (Second Logical Biennial, Summer school&conference, Bulgaria, 1988), (Third Logical Biennial, Summer school&conference, Bulgaria, 1990), на Азиатской логической конференции (The Fourth Asian Logic Conference, Japan, 1990), на конференции по логике в информатике (Annual Conference of the European Association for Computer Science Logic, Poland, 1994), на научных семинарах Московского (1981-1996), Новосибирского (1981, 1983, 1988, 1991) и Тверского госуниверситетов (1980-1996), Амстердамского (1993) и Берлинского (1995) математических институтов.

Публикации Основные результаты диссертации содержатся в [1], [2], [3], [4], [9], [10], [14], [15], [16], [19], [20], [21], [22], [23], [24], [25], [26], [27], [28], [29], [30], [31], [32], [33], [34], [35], [36], [37], [38], [39], [40], [41], [42], [44], [45], [46], [47], [48], [49], [50], [51], [52], [53], [54], [55], [56], [57], [58], [59], [60], [61], [43], [62], [63]; в том числе, большая их часть представлена в монографическом виде в [62].

Структура и объём работы Диссертация состоит из введения (на 14 страницах) и пяти глав, структурированных по разделам и, в некоторых случаях, по подразделам. Общий объем текста — 292 страницы, в тексте содержится 45 рисунков. Список литературы (на 18 страницах) содержит 154 наименования.

СОДЕРЖАНИЕ РАБОТЫ

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

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

В разделе 1.2 представлен фрагмент теории полных по Посту (то есть непротиворечивых, но не имеющих собственных непротиворечивых расширений) логик, разработанной диссертантом в [15], основное приложение которой в данной работе относятся к разрешимым свойствам расширений СЬ в разделе 4.2 и неразрешимым свойствам Б в подразделе 5.2.3. Одним из примеров доказанных здесь утверждений10 является

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

Помимо этого, в разделе 1.2 рассматривается введённое диссертантом понятие обобщённо полной по Посту логики: логика обобщённо полна по Посту, если она непротиворечива и после постулирования всех допустимых в ней правил вывода не имеет собственных непротиворечивых расширений. Доказывается

Теорема. Логика Ь обобщённо полна по Посту тогда и только тогда, когда многообразие её матриц порождается О-порождённой матрицей. Если фильтр выделенных элементов этой матрицы является ультрафильтром, то логика Ь полна по Посту.

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

иТо есть строящимися без использования переменных, из константы 1. (««ложь»») с помощью всех связок.

В разделе 1.3 доказываются два ключевых для доказательств результатов о табличных логиках факта, представляющих и самостоятельный интерес в теории модальных логик: первый из них — формульный критерий табличности логики, второй — конечная аксиоматизируемость табличных логик во всех рассматриваемых семействах логик. Наконец, в разделе 1.4 определяется основная используемая в работе формализация понятия алгоритма — машины Минского — и доказывается техническое утверждение: существуют такие машина Минского и начальные данные для неё, что алгоритмически неразрешима проблема получения интересующих нас данных с помощью этой машины из этих начальных данных.

В главе 2 основной вопрос исследования — разрешимость логики. В частности, рассматриваются критерии разрешимости. Одним из наиболее часто упоминаемых критериев разрешимости является критерий Харропа12: если логика конечно-аксиоматизируема и финитно аппроксимируема, то она разрешима. В разделе 2.1 доказаны следующие две теоремы, показывающие, что условия критерия Харропа невозможно ослабить.

Теорема. Существуют (нормальные13 модальные, суперинтуиционистские) неразрешимые рекурсивно аксиоматизируемые финитно аппроксимируемые логики.

Теорема. Существуют (нормальные модальные, суперинтуиционистские) неразрешимые логики, задаваемые разрешимыми классами конечных шкал111.

12Сы. [R.Harrop. On the existence of finite models and decision procedures for propositional calculi // Proc. Cambridge Philos. Soc., 1958, v. 54, p. 1-13.], где он сформулирован применительно к исчислениям очень общего вида.

13То есть замкнутых по правилу Гёделя <р/0<р.

14 Термин 'шкала' является устоявшимся в теории неклассических логик названием для реляционных семантических структур.

Заметим, что логика разрешима тогда и только тогда, когда она рекурсивно аксиоматизируема и задается рекурсивным классом рекурсивных алгебр15. Известны проблемы А.В.Кузнецова16, касающиеся аппроксимируемости суперинтуиционистских логик рекурсивными алгебрами. Решением некоторых связанных с ними проблем является

Теорема. (¡) Существуют (нормальные модальные, суперинтуицио-пистские) логики, не аппроксимируемые рекурсивными алгебрами.

(и) Существуют полные по Крипке (нормальные модальные, суперинтуиционистские) логики, не аппроксимируемые рекурсивными шкалами.

В разделах 2.2 (разделенном на три подраздела в соответствии с рассматриваемыми классами логик), 2.4, 2.5 и 2.6 проводится моделирование машин Минского средствами пропозициональных логик из различных классов — временных, модальных, суперинтуиционистских. При этом учитываются два важнейших фактора: пригодность получаемого моделирования для дальнейших приложений, которые приводятся в последующих главах, и ««экономность»» используемых для моделирования средств, в частности •— снижение числа применяемых переменных. Для решения последней задачи диссертантом был разработан метод контекстных подстановок. Его первое использование в наиболее ясной форме содержится в разделе 2.3, где доказываются следующие два утверждения.

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

16См. [Логическая тетрадь. Новосибирск, ИМ СО АН СССР, 1986.], проблемы 95, 96.

Теорема. В нормальных расширениях СЬ17 существует исчисление, аксиоматизируемое дополнительными формулами с не более чем одной переменной, для которого неразрешима проблема выводимости формул с одной переменной.

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

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

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

—■(г/ А и) V —•(—А и) V А -пи) V А -т)

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

173десь вЬ обозначает логику доказуемости в формальной арифметике, которая ахсиомаяизируется так: вЬ — К © 0(С1р р) —> Пр, Дальнейшие обозначения модальных и еуперингущдаонистских логик стандартны. Отметим только, что символ ф, в отличие от +, означает постулирование правила Гёделя.

тат содержится в разделе 2.4). Другой пример такого рода: в разделе 2.2 и в разделах 5 главы приводятся константные неразрешимые в нормальных модальных логиках формулы, в частности: в нормальных модальных логиках неразрешима формула ÜJ_, однако разрешимы её отрицание ->□.! и обе формулы _L, Т = ~>JL

Бели в главе 2 по существу рассмотрены с алгоритмической точки зрения два вида следования: дедуктивная выводимость, выражаемое формально отношением Ь, и семантическое следование, то есть отношение то в главе 3 изучаются некоторые близкие к ним понятия ■— допустимые правила вывода, производные правила вывода, следование на конечных шкалах, первопорядковая определимость модальных формул на конечных шкалах18, которые также являются вариантами логического следования.

В разделе 3.1 строится разделяющий пример для проблемы разрешимости проблемы допустимости правил вывода в данной логике — разрешимая логика, проблема допустимости правил вывода в которой неразрешима. Это даёт ответ на довольно естественный вопрос, связанный с тем, что в 80—90- годы для многих представляющих интерес логик проблема допустимости правил вывода решалась положительно19, а всякая неразрешимая логика имеет, конечно, неразрешимую. В данном разделе, помимо прочего, строится разрешимая логика с неразрешимой проблемой производности правил вывода и рассматриваются аналогичные задачи для эквациональных логик.

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

1'Напомним, что модальная формула <р является первопорядково определимой в классе шкал С, если существует такая классическая формула первого порядка ф, что и ф истинны на одних и тех же шкалах из класса С.

19См., например, [V.V.RybaKOV. Criteria/от admissibility of inference rules. Modal and intermediate logics with the branching property. // Studia Lógica. 1994. V. 53. P. 203-226.].

мых исчислений не дают непостредственно ответ на довольно старый и естественный вопрос о разрешимости семантического следования на конечных шкалах: определить для двух формул, верно ли, что вторая истинна в тех конечных шкалах, в которых истинна первая. Отметим, что этот вопрос допускает разнообразные уточнения, связанные с тем, что мы может рассматривать разные типы формул — интуиционистские, мономодальные, многомодальные и пр., выбирать шкалы из разных классов — без каких-либо ограничений, рассматривать в случае, скажем, модальных формул только транзитивные шкалы и т.п., рассматривать варианты следования в локальном варианте: для формул <р считать, что формула ф локально финитарно семантически следует из формулы (р, если ф истинна в каждой точке каждой конечной шкалы, в которой (точке) истинна (р. В разделе 3.2 приводится конструкция, дающая отрицательный ответ на вопрос о разрешимости семантического следования на конечных шкалах для модальных формул, а в разделе 3.4 эта конструкция модифицируется для случая интуиционистских формул и интуиционистских шкал.

Раздел З.З20 посвящён алгоритмическому сравнению выразительной силы модальных формул с выразительной силой классических формул первого порядка. Доказывается

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

В 4 и 5 главах рассматриваются алгоритмические проблемы, связанные со свойствами логик: результаты 4-й относятся к ««положительному»» направлению исследований, 5-й — к ««отрицательному»».

В разделах 4.1 и 4.2 рассматриваются свойства расширений логики вЬ: в 4.1 — нормальных, в 4.2 — произвольных. В частности, в

^Результаты этого раздела принадлежат нераздельному авторству диссертанта и Л.А.Чагровой.

разделе 4.1 доказываются следующие теоремы.

Теорема. Проблема табличности нормальных расширений вЬ алгоритмически разрешима.

Теорема. Проблема локальной табличности нормальных расширений вЬ алгоритмически разрешима.

Аналоги этих утверждений доказаны в разделе 4.2 и для ExtGL. Кроме них, в этом разделе доказываются следующие два результата.

Теорема. Проблема антитабличности21 расширений СЬ разрешима.

Теорема. Пусть X — некоторое конечное или коконечное множество полных по Посту расширений вЬ. Тогда свойство иметь X в качестве множества полных по Посту расширений разрешимо в расширениях СЪ.

Из последнего утверждения при X — 0 получается важнейшее

Следствие. Свойство непротиворечивости расширений ОЬ разрешимо.

Кроме того, здесь доказывается

Теорема. Всякая константная формула разрешима в Ех1СЬ.

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

сг0 - ±, ак=ркУ Щрк <Тк-1), к>0.

Например, доказывается

"Логика называется антитабличной, если она непротиворечива и не имеет конечных моделей.

Теорема. Проблема табличности нормальных расширений К4 ф <ут разрешима при любом т, т £ ш.

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

Теорема. Проблема табличности расширений К4 ф ат разрешима при любом т., т & 01.

Еще одним результатом, доказанным в разделе 4.3, является Теорема. Проблема табличности расширений Б4 разрешима.

Эта теорема представляет интерес в связи с приложениями логики Б4 в самых разных областях знаний: она является естественным фрагментом динамической логики при фиксировании одной итерированной программы, кроме того, известны её связи с топологией (топологические пространства являются её адекватной интерпретацией), с интуиционистской логикой; в то же время исследования расширений Б4 неоправданно ограничивалось лишь нормальными её расширениями.

Раздел 4.4 содержит краткую сводку других разрешимых свойств логик, большей частью рассмотренных диссертантом, но не относящихся к основным результатам диссертации. Материал этого раздела предназначен для сравнения с результатами главы 5.

В главе 5 показано, что довольно бедный набор разрешимых свойств, представленный в главе 4, — далеко не случайность, что на самом деле большинство интересных свойств в основных интересных классах логик неразрешимы.

В разделе 5.1 для класса суперинтуиционистских логик доказывается неразрешимость многих стандартных свойств22, таких как: разрешимость, финитная аппроксимируемость (подраздел 5.1.1); пол-

22Что составляет решение известной проблемы Л.Л.Максимовой, см. ¡Логическая тетрадь. Новосибирск, ИМ СО АН СССР, 1986.], проблема 100.

нота по Крипке (подраздел 5.1.2), дизъюнктивное свойство23, полнота по Холдену (подраздел 5.1.3); допустимость дизъюнктивного свойства (подраздел 5.1.4). Как следствие, с помощью известных теорем о переносе и других приемов в подразделе 5.1.5 получаются аналогичные результаты для нормальных расширений 84.

В разделе 5.2 в трёх различных классах (они рассматриваются в подразделах 5.2.1, 5.2.2, 5.2.3, соответственно) расширений логики СЬ — КЕх1СЬ, Ех1СЬ, Ех1Б — изучаются неразрешимые свойства логик. Здесь помимо явных аналогий по сравнению с предыдущим разделом получены некоторые результаты, не имеющие аналогов в суперинтуиционистских логиках и расширениях Б4. Так, доказывается

Теорема. Следующие свойства неразрешимы в NExtGL.• разрешимость, финитная аппроксимируемость, полнота по Крипке, интерполяционное свойство24, дизъюнктивное свойство.

Содержательно осмысленным в расширениях СЬ ввиду их арифметической интерпретации, при которой □ понимается как доказуемость, является правило вывода С1<р/<р. Доказана

Теорема. Допустимость правила вывода Скр/ср неразрешима в NExtGL.

К ««обратному»» к этому правилу относится

Теорема. Свойство нормальности неразрешимо в Ех1СЬ.

В подразделе 5.2.3 доказана

23Этот результат получен совместно диссертантом и М.В.Захарьягцевым.

24Это свойство в соответствии с известными результатами Л.Л.Максимовой 1977 г. и 1979 г. разрешимо в суперинтуиционистских логиках и в нормальных расширениях 84.

Теорема. Следующие свойства неразрешимы в ExtS: разрешимость25, интерполяционное свойство, полнота по Холдену26.

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

В подразделе 5.3.1 доказываются следующие два факта.

Теорема. Проблема табличности нормальных модальных логик неразрешима.

Теорема. Проблема локальной табличности нормальных модальных логик неразрешима.

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

Теорема. Пусть V — конечно-аксиоматизируемое непротиворечивое нормальное расширение логики КО = Кф ОТ. Тогда проблема совпадения нормального расширения К с Ь' неразрешима.

Теорема. Пусть Ь' — конечно-аксиоматизируемое непротиворечивое нормальное расширение логики К4. Тогда проблема совпадения нормальной модальной логики с Ь' неразрешима.

Кроме того, из результатов подразделов 5.3.1 и 5.3.2 следует

Теорема. Противоречивая логика — это единственная табличная нормальная модальная логика, проблема совпадения которой с произвольной нормальной модальной логики разрешима.

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

26Это свойство разрешимо в нормальных расширениях ОЬ.

В подразделе 5.3.3 доказывается

Теорема. Свойство аксиоматизируемости константными аксиомами неразрешимо в МЕхкК4 и в NExtK.

Отметим, что оба утверждения этой теоремы независимы. Для иллюстрации этого обстоятельства здесь же, в подразделе 5.3.3 строится финитно аппроксимируемая нормальная модальная логика Ь и константная формула, что нормальное расширение Ь этой формулой финитно аппроксимируемой не является, построение аналога которого в ИЕх1К4 невозможно.

В подразделе 5.3.4 рассматривается вопрос, относящийся к традиционной проблематике модальной логики, имеющей, впрочем, значение и для алгоритмических исследований, скажем, динамических логик: вопрос о конечности множества несводимых модальностей. Под модальностью понимается слово в алфавите {-!,□}, а две модальности М\ к Л/2 считаются сводимыми в логике Ь, если Ь Ь М\р <-¥ М2р; например, К, К4, вЬ имеют бесконечные множества несводимых модальностей, а Б4 — четырнадцать.

Теорема. Свойство иметь конечное множество несводимых модальностей неразрешимо в КЕхЖ.

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

Теорема. Свойство непротиворечивости неразрешимо в МЕхЖ4<;. (и) Свойство непротиворечивости неразрешимо в ЕхЖ4.

Библиография

[1] М.В.Захарьящев, А.В.Чагров. Неразрешимость дизъюнктивного свойства суперинтуиционистских исчислений. Препринт йн. прикл. матем. им. М.В.Келдыша АН СССР. N 57. 1989 г.

[2] М.В.Захарьящев, А.В.Чагров. Неразрешимость свойства полноты по Холдену модальных исчислений. Препринт Ин. прикл. матем. им. М.В.Келдыша АН СССР. N 82. 1990 г.

[3] М.В.Захарьящев, А • В.чагров. О полноте по Холдену // Десятая Всесоюзная конференция по математической логике. Алма-Ата, 1-3 ноября 1990 года / Алма-Ата, Гылым, 1990, с. 70.

[4] А.и.циткин, А.В.Чагров. Об аппроксимируемости многообразий псевдобулевых алгебр // XIX Всесоюзная алгебраическая конференция. Львов, 9-11 сентября 1987 г. Тезисы сообщений, часть первая. Львов, 1987, с. 305.

[5] А.В.Чагров. Суперинтуиционистские фрагменты ненормальных модальных логик // Математическая логика и математическая лингвистика. Калинин, КГУ, 1981, с. 144-162.

[6] А.В.Чагров. О ненормальных модальных напарниках Int // Автоматы, алгорифмы, языки. Калинин, КГУ, 1982, с. 133-148.

[7] А.В.Чагров. Числа Куратповского // Применение функционального анализа в теории приближений. Калинин, КРУ, 1982, с. 186-190.

[8] А.В.ЧАГРОВ. О некоторых свойствах расширений модальной логики S3 // Модальные и интенсиональные логики. Материалы VIII Всесоюзной конфереции ««Логика и методология науки»». Вильнюс, 1982, с. 123-124.

[9] А.В.Чагров. Неклассические логики и многообразия логических матриц // Семиотические аспекты формализации интеллектуальной деятельности. Школа-семинар ««Телави-83»». Тезисы докладов и сообщений. М., 1983, с. 136-138.

[10] А.В.Чагров. О минимальных модальных напарниках Int // Семиотические аспекты формализации интеллектуальной деятельности. Школа-семинар ««Телави-83»». Тезисы докладов и сообщений. М., 1983, с. 138-140.

[11] А.В.Чагров. О полиномиальной финитной аппроксимируемости модальных и суперинтуиционистских логик // Математическая логика, математическая лингвистика и теория алгоритмов. Калинин, КГУ, 1983, с. 75—83.

[12] А.В.ЧАГРОВ. О сложности суперинтуиционистских логик // Седьмая Всесоюзная конференция по математической логике. Новосибирск, ИМ СО АН СССР, 1984, с. 193.

[13] А.В.Чагров. О сложности пропозициональных логик // Слож-ностные проблемы математической логики. Калинин, КГУ, 1985, с. 80-90.

[14] А.В.ЧАГРОВ. 0-порождённые логические матрицы, порождаемые ими многообразия и полнота по Посту // XVIII Всесоюз-

пая алгебраическая конференция. Кишинёв, 16-18 сентября 1985 г. Тезисы сообщений. Часть вторая. Кишинёв, 1985, с. 262.

[15] ЧАГРОВ A.B. Многообразия логических матриц // Алгебра и логика. 1985. Т. 24. N 4. С. 426-489.

[16] А.В.чагров. Простые примеры неразрешимых рекурсивно аксиоматизируемых финитно аппроксимируемых эквациональных логик // Восьмая Всесоюзная конференция по математической логике. М., 1986, с. 206.

[17] А.В.чагров. Два континуума максимальных пропозициональных логик // Логика и системные методы анализа научного знания. Тезисы докладов к IX Всесоюзному совещанию по логике, методологии и философии науки. Харьков, 8-10.Х.1986. М., 1986, с. 50-51.

[18] А.В.чагров. Нижняя оценка мощности аппроксимирующих шкал Крипке // Логические методы построения эффективных алгоритмов. Калинин, КГУ, 1986, с. 96-125.

[19] А.в.чагров. Две теоремы об эквациональных логиках в сигнатуре из двух унарных символов // Логико-алгебраические конструкции. Калинин, КГУ, 1987, с. 90-96.

[20] А.В.Чагров. Два новых вида мультимодальных логик // Неклассические логики и пропозициональные установки. М., ИФ АН СССР, 1987, с. 48-59.

[21] А.В.чагров. Несколько замечаний о свойствах итерации //II Всесоюзная конференция по прикладной логике. Новосибирск, 7-9 июня 1988 г. Тезисы докладов. Новосибирск, 1988, с. 237-239.

[22] А.в.члгров. Некоторые свойства логических эквационалъных логик // Девятая Всесоюзная конференция по математической логике. Л., Наука, 1988, с. 172.

[23] А.В.ЧлГРОВ. Нетабличпостъ — предтабличность, антитаб-личностъ, коантитабличиостъ // Алгобро-логические конструкции. Калинин, КГУ, 1989, с. 105-111.

[24] А.В.Чагров. О границах множества модальных напарников интуиционистской логики ¡1 Неклассические логики и их применения. М., ЙФ АН СССР, 1989, с. 74-81.

[25] А.В.Чагров. Добавление к статье Л.А.Чагровой О неразрешимости первопорядковой определимости пропозициональных формул // Неклассические логики и их применения. М., ЙФ АН СССР, 1989, с. 84-85.

[26] А.В.чагров. Неразрешимость финитарного семантического следования //Десятая Всесоюзная конференция по математической логике. Алма-Ата, 1-3 ноября 1990 года / Алма-Ата, Гылым, 1990, с. 162.

[27] А.В.Чагров. Погружения интуиционистской логики в альтернирующую пропозициональную динамическую логику // X Всесоюзная конференция по логике, методологии и философии науки. Тез. докл. и выст. / Минск, БелНИИНТИ, 1990, с. 96-97.

[28] А.В.ЧАГРОВ. Неразрешимые свойства расширений логики доказуемости Ц Алгебра и логика. 1990. Т. 29. N 3. С. 350-367.

[29] А.В.Чагров. Неразрешимые свойства расширений логики доказуемости. II// Алгебра и логика. 1990, Т. 29. N 5. С. 613-623.

[30] А.В.Чагров. Разрешимая модальная логика с неразрешимой проблемой допустимости правил вывода ]/ Алгебра и логика. 1992. Т. 31. N 1. С. 83-93.

[31] А.В.Чагров. Континуальность множества максимальных су-перинтуициопистских логик со свойством дизъюнктивности // Математические заметки. 1992. Т. 51, вып. 2. С. 117-123.

[32] А.В.ЧАГРОВ. О рекурсивной аппроксимируемости модальных и суперинтуиционистских логик // Алгебраические и логические конструкции. Тверь, ТГУ, 1994, с. 91-97.

[33] А.В.Чагров. Неразрешимые свойства суперинтуиционистских логик // Математические вопросы кибернетики. Вып. 5: Сборник статей/ Под ред. С.В.Яблонского. М., Физматлит, 1994, с. 62-108.

[34] А.В.Чагров, Л.А.Чагрова. Разрешимость проблемы апти-табличности расширений логики Гёделя-Лёба // Логические методы построения эффективных алгоритмов. Калинин, КГУ, 1986, с. 126-129.

[35] А.В.Чагров, Л.А.Чагрова. О первопорядковой определимости интуиционистских формул в классе шкал высоты не более трёх // Конструкции в алгебре и логике. Тверь, ТГУ, 1990, с. 117119.

[36] A.V.Chagrov. Possibilities of the classical interpretations of intuitionistic logic // Proc. 8th International Congress of Logic, Meth. and Phil. Science, Moscow (August 1987). M., Nauka, 1987. V. 5. Part 1. P. 237-239.

[37] A.V.Chagrov. Undecidability in propositional logics: calculi, formulas, properties // Third Logical Biennial, Summer

school&conference in honour of S. C. Kleene. June 6-15, 1990; Chaika near Varna; Bulgaria. Sofia, 1990, p. 14.

[38] A.ChagROV. Four intervals of irreducible logics // Bulletin of the Section of Logic. 1993. Vol. 22. No. 4. P. 167-168.

[39] A.Chagrov. Some remarks about generalized Post-completeness of extensions of K4 // Bulletin of the Section of Logic. 1994. Vol. 23. No. 1. P. 27-29.

[40] a.chagrov. The undecidability of the tubularity problem for modal logic // Logic Colloquium'94. Abstr. of contributed papers. Clermont-Ferrand, France, 21-30 juilett 1994. 1994. P. 34.

[41] a.chagrov. a note on expressive power of iteration j/ Bulletin of the Section of Logic. 1995. Vol. 24. No. 4. P. 234-235.

[42] A.Chagrov. One more first order effect in Kripke semantics // Proc. of the 10th International Congress of Logic, Methodology and Philosophy of Science. 1995, Florence, Italy, p. 175.

[43] a.chagrov. The undecidability of the tabularity problem for modal logic // Bull. Symbol. Log. 1995. Vol. 1. No. 2. P. 228.

[44] A.V.Chagrov, L.A.Chagrova. Algorithmic problems concerning first-order definability of modal formulas on the class of all finite frames. Preprint, ILLC Prepublication Series for Mathematical Logic and Foundations, ML-93-07, University of Amsterdam, 1993.

[45] A.V.Chagrov, L.A.Chagrova. Algorithmic problems concerning first-order definability of modal formulas on the class of all finite frames // Studia Logica. 1995. V. 55. No. 3. P. 421-448.

[46] A.V.Chagrov, V.B.Shehtman. Algorithmic aspects of tense logics // L.Pacholski, J.tluryn (Eds.) Computer Science Logic, 8th Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994. Selected Papers. Springer, Lecture Notes in Computer Science, 1995, v. 933, pp. 442-455.

[47] A.V.Chagrov, M.v.zakharyashchev. Five theorem about the disjunction property of intermediate logics // Международная конференция по алгебре, посвященная памяти А.И.Мальцева (1909-1967). Тезисы докладов по теории моделей и алгебраических систем. Новосибирск, ИМ СО АН СССР, 1989, с. 45.

[48] A.V.Chagrov, M.V.zakharyashchev. Five theorem about the disjunction property of intermediate logics j/ ASL Logic Colloquium 'Berlin 89'. Abstracts, 1989.

[49] A.V.Chagrov, M.V.zakharyashchev. On Hallden-completeness of intermediate and modal logics // Bulletin of the Section of Logic. 1990. V. 19. No. 1. P. 21-24.

[50] A.Chagrov,

m.zakharyashchev. Modal companions of intermediate logics: A survey ¡j Third Logical Biennial, Summer school&conference in honour of S.C.Kleene. June 6-15,1990. Bulgaria, Sofia, 1990, p. 15.

[51] A.Chagrov, m.zakharyashchev. An essay in complexity aspects of intermediate calculi // Proceedings of the Fourth Asian Logic Conference. Tokyo, 1990, p. 26 - 29.

[52] A.Chagrov, M.Zakharyashchev. The disjunction property of intermediate propositional logics. Preprint, University of Amsterdam, ITLI Prepublication Series, X-91-01, 1991.

[53] A.Chagrov, M.Zakharyashchev. Undecidability of the disjunction property of intermediate propositional logics.

Preprint, University of Amsterdam, ITLI Prepublication Series, X-91-02, 1991.

[54] A.Chagrov,

m. zakharyashchev. Modal Companions of Intermediate Propositional Logics // Studia Logica. 1991. V. 51. No. 1. P. 49-82.

[55] A.Chagrov, M.Zakharyashchev. The disjunction property of intermediate propositional logics // Studia Logica. 1991. V. 50. No. 2. P. 189-216.

[56] A.Chagrov, M.Zakharyashchev. The Sahlqvist formulas are not so elementary // The 1992 Europian Summer Meeting of the ASL. Vesprem, August 9 to 15, 1992. Abstracts. J.Bolyai Mathematical Society, 1992, p. 75.

[57] A.Chagrov, M.Zakharyashchev. The undecidability of the disjunction property of propositional logics and other related problems // J. Symb. Log. 1993. V. 58. No. 3. P. 967-1002.

[58] A.Chagrov, M.Zakharyashchev. The Sahlqvist formulas are not so elementary // J. Symb. Log. 1993. V. 58. No. 3. P. 1137-1138.

[59] A.Chagrov, M.Zakharyashchev. On the independent axiomatizability of modal and intermediate logics. Preprint, ILLC Prepublication Series for Mathematical Logic and Foundations, ML-93-17, University of Amsterdam, 1993.

[60] A.Chagrov, M.zakharyaschev. Sahlqvist formulas are not so elementary even above S4 // Logic Colloquium '92 (edited by Laslo Csirmaz, Dov M. Gabbay and Maarten de Rijke). CSLI (Center for the Study of Language and Information) Publications (& Folli

(The European Association for Logic, Language and Information)), Stanford, California, 1995, pp. 61-73.

[61] A.ChaGROV, M.ZAKHARYASCHEV. On the independent axiomatizability of modal and intermediate logics //J. Logic Computat. 1995. V. 5. No. 3. P. 287-302.

[62] A.Chagrov, M.zakharyaschev. Modal Logic. Oxford University Press, 1997.

[63] M.zakharyaschev, F.Wolter, A.ChaGROV. Advanced Modal Logic. Preprint IS-RR-96-0027F (ISSN 0918-7553), School of Information Science, Japan Advanced Institute of Science and Technology, Hokuriku, 1996.

ТвГУ. Тираж 100 экз. Заказ 205.

РОССИЙСКАЯ АКАДЕМИЯ НАУК ИНСТИТУТ ПРОБЛЕМ ПЕРЕДАЧИ ИНФОРМАЦИИ РАН

на правах рукописи

ЧАГРОВ Александр Васильевич

МОДЕЛИРОВАНИЕ ВЫЧИСЛИТЕЛЬНЫХ ПРОЦЕССОВ СРЕДСТВАМИ ПРОПОЗИЦИОНАЛЬНЫХ ЛОГИК

Специальности: 05.13.17 — Теоретические основы информатики 01.01.06 — Математическая логика, алгебра и теория чисел

Диссертация на соискание учёной степени доктора физико-математических наук

Научный консультант: профессор, доктор физико-математических наук В.А.Любецкий

Москва 1998

О главление

ОГЛАВЛЕНИЕ 1

ВВЕДЕНИЕ 4

Общая характеристика работы ......................................4

Краткий исторический очерк ......................................................14

1 ИСХОДНЫЕ ОПРЕДЕЛЕНИЯ И ФАКТЫ 18

1.1 Модальные и суперинтуиционистские логики..............................18

1.2 Полнота по Посту..............................................................28

1.3 Табличные логики..............................................................38

1.4 Машины Минского ............................................................43

2 О РАЗРЕШИМОСТИ ЛОГИК 46

2.1 Об обобщениях критерия Харропа разрешимости логик.........46

2.2 Моделирование машин Минского модальными средствами с использованием константных формул..................................................54

2.2.1 Случай временных логик..............................................55

2.2.2 Случай расширений К4................................................60

2.2.3 Случай расширений вГ ..............................................68

2.3 Метод контекстных подстановок..............................................74

2.4 Моделирование машин Минского средствами супер интуиционистских логик ...................................... 78

2.5 «Экономные» неразрешимые суперинтуиционистское исчисление и неразрешимая формула............................. 86

2.6 «Экономные» неразрешимые исчисление и неразрешимая формула в NExtS4..................................... 98

3 АЛГОРИТМИЧЕСКИЕ ПРОБЛЕМЫ СЛЕДОВАНИЯ 105

3.1 Разрешимая модальная логика с неразрешимой проблемой допустимости правил вывода...............................105

3.2 Проблема семантического следования модальных формул на конечных шкалах...................................116

3.3 О первопорядковой определимости модальных формул на конечных модальных шкалах ..............................128

3.4 О финитарном семантическом следования на конечных интуиционистских шкалах..................................152

4 ОБ АЛГОРИТМИЧЕСКОМ ОПИСАНИИ СВОЙСТВ ЛОГИК: РАЗРЕШИМЫЕ СВОЙСТВА 161

4.1 Табличность в NExtGL............................162

4.2 Разрешимые свойства в ExtGL .......................169

4.3 К проблеме табличности в NExtK4.....................178

4.4 Еще несколько примеров разрешимых свойств ..............183

5 ОБ АЛГОРИТМИЧЕСКОМ ОПИСАНИИ СВОЙСТВ ЛОГИК: НЕРАЗРЕШИМЫЕ СВОЙСТВА 188

5.1 Неразрешимые свойства суперинтуиционистских логик.........188

5.1.1 Схема доказательств неразрешимости свойств исчислений. Разрешимость и финитная аппроксимируемость ...........189

5.1.2 Полнота по Крипке..........................192

5.1.3 Полнота по Холдену, полнота по Максимовой и дизъюнктивное свойство.................................201

5.1.4 Допустимость дизъюнктивного свойства..............212

5.1.5 О нормальных модальных напарниках суперинтуиционистских логик..................................219

5.2 Неразрешимые свойства в расширениях логики СЬ ...........227

5.2.1 Неразрешимые свойства в МЕх1СЬ.................229

5.2.2 Неразрешимые свойства в Ех1СЬ..................244

5.2.3 Неразрешимые свойства в Ех18...................246

5.3 Неразрешимые свойства нормальных модальных логик.........255

5.3.1 Логики, не содержащие ОТ.....................256

5.3.2 Непротиворечивые логики, содержащие ОТ............260

5.3.3 Проблема аксиоматизируемости константными формулами . . . 263

5.3.4 Нормальные модальные логики с конечным числом несводимых модальностей...........................269

5.4 Неразрешимые свойства логик в ЕхЖ4 и в ИЕхЖ^ при п > 1.....273

Литература 275

В В ЕДЕН И Е Общая характеристика работы

Актуальность темы исследования В 70——80— годы было досрочно подтверждено предвидение создателя языка лисп Дж.Маккарти, высказанное им в 1967 году: «Разумно ожидать, что связи между вычислительной техникой и математической логикой окажутся столь же плодотворными в следующем столетии, какими были связи между математическим анализом и физикой в столетии предыдущем». Оказалось, что в плодотворности этих связей можно убедиться уже в наши дни1. Методы математической логики дали возможность осуществить многие новые подходы к созданию вычислительных средств, баз данных, экспертных систем, языков программирования, синтезу и верификации программ и пр. При этом действенной оказалась и обратная связь: возникли новые разделы математической логики, оказались по-

1В предисловии редакторов сборника переводов [30] сказано, например: «Чтобы представить себе, хотя бы в общих чертах, те направления, в которых развивается современная вычислительная наука, полезно взглянуть на названия сборников широко известной серии Lecture Notes in Computer Science, выпускаемой западногерманским издательством Springer-Verlag и содержащей материалы многих международных конференций по информатике. ... чуть ли не на каждой пятой обложке можно увидеть термины «логический вывод», «логическое программирование», «компьютерная логика», «логики программ» и т.д. ». Ещё раньше плодотворность применения средств математической логики в программировании была блестяще продемонстрирована в [120].

новому расставленными акценты в ряде её традиционных разделов. Практически в каждом справочном пособии и многих монографиях по информатике или искусственному интеллекту математическая логика выступает и в качестве языка обсуждения предмета, и в качестве необходимой компоненты представления результатов, и в качестве инструмента для их получения2. Сейчас происходит переосмысление всего здания логики с учетом этой новой реальности: те её части, которые до того считались неклассическими и представляли собой нечто экзотическое, становятся едва ли не главными объектами исследований и приложений3. При этом особый интерес представляют логические системы, имеющие реляционное истолкование (в частности, и в форме семантики): программные и динамические логики, модальные и многомодальные (особенно временные), интуиционистская4 и близкие к ней логики.

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

2См., например, [79], [126], [128], [127], [153].

3Авторы [33] говорят по этому поводу: «С точки зрения названных задач перспективной кажется и разработка математических исчислений так называемой модальной логики, оперирующей, наряду с традиционными для классической логики оценками «истинно» и «ложно», также и такими

оценками, как «возможно», «необходимо», «правдоподобно», «произойдёт в будущем» и т.д.».

4 Интуиционистская логика оказалась пригодной для описания свойств вычислений даже в тех

случаях, когда логики на классической основе не давали непосредственной возможности для их использования, например: синтеза программ [2], [29], для описания альтернирующих вычислений [58],

моделирования немонотонных рассуждений [118].

5Рост значения модальной логики для информатики можно охарактеризовать таким фактом.

Авторы монографии [149] отвели модальной логике в первом томе своего сочинения около 5%

достаточным для проявления практически всех «неклассических» эффектов, полезных для приложений, и для подходящего развития логических систем на базе более богатых по выразительным возможностям логических языков — первого и более высоких порядков.

В соответствии с подразумеваемыми приложениями представляется весьма актуальным изучение эффективных представлений вычислений в пропозициональных логиках, причем эти представления имеют два диаметрально противоположных аспекта — «положительный», связанный с построением конкретных алгоритмов, решающих массовые задачи, связанные с логиками, такие как выводимость формулы в исчислении, допустимость и/или производность правила вывода в логике, выяснение выполнимости свойства в логике и т.д., и «отрицательный», характеризующийся отсутствием соответствующих алгоритмов. Кавычки здесь поставлены потому, что на самом деле оба аспекта положительны: «положительный» — ввиду предоставления конкретных алгоритмов, которые в определённых случаях можно применять для решения прикладных задач, а «отрицательный» — ввиду того, что при доказательстве неразрешимости как составная часть используется непосредственное представление алгоритмов в исчислениях, то есть разрабатываются выразительные возможности языка пропозициональных логик, чем расширяется область их приложений6.

объёма текста, а второй том снабдили подзаголовком «От модальной логики к логике баз данных».

6Кроме того, стоит иметь в виду и другой очевидный аспект «отрицательных» результатов, см. [33]: «Понимание, что в принципе невозможно сделать что-то, имеет для программирования не меньшее значение, чем для техники невозможность нарушить второе начало термодинамики или для физики невозможность превысить скорость света».

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

• представление вычислений средствами логического следования:

— в виде выводов в исчислениях;

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

— в виде допустимых в данной логике правил вывода; их наличие может существенно ускорить алгоритмы, распознающие принадлежность формул этой логике;

• алгоритмическое описание свойств реляционных структур средствами пропозициональных языков:

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

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

приложений в рассматриваемой совокупности задач средства хорошо разработанной теории моделей классической логики первого порядка;

• алгоритмическое описание свойств логик:

- выяснение по аксиоматизации логики ее семантических свойств, таких как:

* финитная аппроксимируемость, то есть возможность ограничения класса адекватных для логики структур конечными;

* реляционная полнота, то есть точность соответствия логики и класса моделирующих её реляционных структур;

* табличность логики, то есть её адекватность по отношению к одной конечной реляционной структуре;

— выяснение по аксиоматизации логики ее внутренних свойств, таких как7:

* непротиворечивость, то есть нетривиальность логики для дальнейших приложений;

* разрешимость самой логики, разрешимость проблем допустимости, производности в ней правил вывода;

* дизъюнктивное свойство, являющееся методологической основой построения большинства алгоритмов, синтезирующих программы по доказательству их существования, и близкие к нему (полнота по Хол-дену, полнота по Максимовой);

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

73десь указываются лишь центральные в некотором смысле свойства.

конструированию объектов по описаниям желаемых взаимоотношениям их с другими объектами.

Целью работы являются:

• изучение феномена алгоритмической разрешимости/неразрешимости пропозициональных логик, в частности — выяснение границ применимости известных критериев разрешимости, например — критерия Харропа;

• создание простых в некотором смысле (удобных для приложений, экономных по числу используемых в аксиоматике переменных) неразрешимых исчислений;

• решение известных проблем, связанных с правилами вывода (в частности, всякая ли разрешимая логика имеет разрешимую проблему допустимости правил вывода) и с вариантами семантического следования (например, следования на конечных реляционных структурах);

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

Методы исследования Основные методы исследования — семантические методы теории модальных и суперинтуиционистских логик, методы теории моделей классической логики первого порядка, методы теории алгоритмов.

Научная новизна В диссертации получены следующие основные новые результаты:

• Построены примеры неразрешимых логик, задаваемых разрешимыми классами конечных шкал (алгебр, моделей); обосновано существование неразрешимых рекурсивно аксиоматизируемых финитно аппроксимируемых логик; показано, что не все логики можно аппроксимировать рекурсивными алгебрами.

• В следующей таблице приведены обнаруженные в диссертации факты о су-

о

ществовании в рассматриваемых классах логик неразрешимых исчислении с малым числом переменных: первая строка, например, означает, что существует неразрешимое суперинтуиционистское исчисление, аксиомы которого используют 4 переменные, а в формулах, для которых неразрешима проблема выводимости в нем, используются 2 переменные; знак = около числа означает, что оценка числа переменных не понижаема, а < — вопрос о понижении числа переменных открыт.

83десь и далее используются стандартизированные в [116] обозначения: (1Ч)Ех^ — класс (нормальных) расширений логики так, ЕхИг^ обозначает класс суперинтуиционистских логик, NExtS4 — класс нормальных расширений модальной логики 84.

Число переменных в

Класс неразрешимых отделяемых

логик исчислениях формулах

ЕхШ1 < 4 = 2

КЕх184 < з = 1

Ех184 < з = 1

= 1 = 1

Ех1СЬ = 1 = 1

ExtS = 1 = 1

№хЖ4 = 1 = 0

ЕхЖ4 = 1 = 0

• Предложено понятие разрешимой/неразрешимой в данном классе логик формулы, которое является двойственным понятию разрешимой/неразрешимой логики, и найдены простые (по числу переменных, используемым связкам, длине) для рассматриваемых классов логик примеры неразрешимых формул.

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

• Доказана неразрешимость семантического следования на конечных шкалах Крипке в различных вариантах (локальном, глобальном) и в разных классах шкал (вЬ-шкалы, 1^-шкалы и др.). Получена также неразрешимость проблемы первопорядковой определимости модальных формул на классе конечных

шкал9.

• Обоснована разрешимость некоторых свойств логик в некоторых классах — в частности, свойство табличности и непротиворечивости расширений СЬ, а для значительного количества стандартных свойств логик, таких как разрешимость, финитная аппроксимируемость, полнота, интерполяционное и дизъюнктивное свойства и т.д., доказана алгоритмическая неразрешимость практически во всех рассматриваемых классах логик, кроме того, установлена граница (не)разрешимости таких свойств, как непротиворечивость, полнота по Холдену.

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

Апробация По результатам диссертации делались доклады на Всесоюзных конференциях по математической логике (Тбилиси, 1982; Новосибирск, 1984; Москва, 1986; Ленинград, 1988; Алма-Ата, 1990, приглашённый доклад), на Всесоюзных алгебраических конференциях (Кишинёв, 1985, Львов, 1987), на IX Всесоюзном совещании по логике, методологии и философии науки (Харьков, 1986), на Ме-

9Результат получен совместно с Л.А.Чагровой; см. сноску на странице 128.

ждународ�