Введение к работе
Актуальность темы исследования В 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.R.OBINSON. 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.HODKWSON & 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.], [Г.Е.Минц, Э.Х.ТЫУГУ. Структурный синтез и неклассические логики J J Тезисы докл. 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 I'intelligence artificielle. 1. De la logique classique a la programmation logique. Bordas, Paris, 1988. (Русский пер.: А.ТЕЙ, П.ГРИБОМОН, Ж.ЛУИ И ДР. Логический подход к искусственному интеллекту. От классической логики к логическому программированию. М., Мир, 1990.)] отвели модальной логике в первом томе своего сочинения около 5% объёма текста, а второй том снабдили подзаголовком ««От модальной логики к логике баз данных»».
конкретных алгоритмов, которые в определённых случаях можно применять для решения прикладных задач, а ««отрицательный»» — ввиду того, что при доказательстве неразрешимости как органическую часть приходится использовать явное представление алгоритма в исчислении и, тем самым, разрабатывать выразительные возможности языка пропозициональных логик, таким образом расширять область их приложений6.
Цель и задачи исследования Среди весьма обширного списка задач, вытекающих из предыдущего пункта, в диссертацию выбраны для рассмотрения следующие ключевые:
представление вычислений средствами логического следования:
в виде выводов в исчислениях;
в виде семантического следования (то есть содержательного следования, когда формулы описывают строение реляционных структур, представляющих собой формализацию совокупности стадий вычисления в их программной взаимосвязи); в частности, финитарного следования, когда все рассматриваемые реляционные структуры предполагаются конечными, что является естественным отражением свойства реальных вычислительных сред;
в виде допустимых в данной логике правил вывода; их наличие может существенно ускорить алгоритмы, распознающие принадлежность формул этой логике;
6Кроме того, стоит иметь в виду и другой очевидный аспект ««отрицательных»» результатов, см. [А.Л.СЕМЁНОВ, В.А.УСПЕНСКИЙ. Математическая логика в вычислительных науках и вычислительной практике // Вестник АН СССР. 1986. N 7. С. 93-103.]: ««Понимание, что в принципе невозможно сделать что-то, имеет для программирования не меньшее значение, чем для техники невозможность нарушить второе начало термодинамики или для физики невозможность превысить скорость света»».
в алгоритмическое описание свойств реляционных структур средствами пропозициональных языков:
построение алгоритмов, отвечающих по произвольно заданной формуле на вопросы о выполнении для семантически ей адекватных реляционных структур желаемых свойств; или доказательство невозможности таких алгоритмов;
выяснение возможности переопределения реляционных свойств модальных, интуиционистских пропозициональных формул
в терминах классических формул первого порядка, реализация которой предоставляет для приложений в рассматриваемой совокупности задач средства хорошо разработанной теории моделей классической логики первого порядка;
алгоритмическое описание свойств логик:
— выяснение по аксиоматизации логики ее семантических свойств,
таких как:
финитная аппроксимируемость, то есть возможность ограничения класса адекватных для логики структур конечными;
реляционная полнота, то есть точность соответствия логики и класса моделирующих её реляционных структур;
табличность логики, то есть её адекватность по отношению к одной конечной реляционной структуре;
— выяснение по аксиоматизации логики ее внутренних свойств,
таких как7:
* непротиворечивость, то есть нетривиальность логики
для дальнейших приложений;
Здесь указываются лишь центральные в некотором смысле свойства.
разрешимость самой логики, разрешимость проблем допустимости в ней различных правил вывода;
дизъюнктивное свойство, являющееся методологической основой построения большинства алгоритмов, синтезирующих программы по доказательству их существования; и близкие к нему свойства (полнота по Холдспу, полнота по Максимовой);
интерполяционное свойство, дающее во многих интересных случаях возможность явного определения на основе существования неявного, то есть возможность конструирования объекта по описанию его желаемых взаимоотношений с другими объектами.
Целью работы являются:
изучение феномена алгоритмической разрешимости/неразрешимости пропозициональных логик; в частности, выяснение границ применимости известных критериев разрешимости, например, критерия Харропа;
создание простых в некотором смысле (удобных для приложений, экономных по числу переменных, используемых в соответствующей аксиоматике) неразрешимых исчислений;
решение известных проблем, связанных с правилами вывода (в частности, всякая ли разрешимая логика имеет разрешимую проблему допустимости правил вывода) и с вариантами семантического следования (например, следования на конечных реляционных структурах);
выяснение возможностей алгоритмического описания свойств логик (точнее, исчислений, ввиду известной теоремы А.В.Кузнецова об алгоритмической неразрешимости нетривиальных свойств рекурсивно задаваемых логик), то есть обоснование разрешимости
или неразрешимости интересующего нас по каким-либо причинам свойства логик.
Методы исследования Основные методы исследования — семантические методы теории модальных и суперинтуиционистских логик, методы теории моделей классической логики первого порядка, методы теории алгоритмов.
Научная новизна В диссертации получены следующие основные новые результаты:
Построены примеры неразрешимых логик, задаваемых разрешимыми классами конечных шкал (алгебр, моделей); обосновано существование неразрешимых рекурсивно аксиоматизируемых финитно аппроксимируемых логик; показано, что не все логики можно аппроксимировать рекурсивными алгебрами.
В следующей таблице
приведены обнаруженные в диссертации факты о существовании в рассматриваемых классах логик8 неразрешимых исчислений с малым числом переменных: первая строка, например, означает, что существует неразрешимое суперинтуиционистское исчисление, аксиомы которого используют 4 переменные, а в формулах, для которых неразрешима проблема выводимости в нем, используются 2 переменные; знак — около числа означает, что оценка числа переменных не понижаема, а < — вопрос о понижении числа переменных открыт.
Предложено понятие разрешимой/неразрешимой в данном классе логик формулы, которое является двойственным понятию разрешимой/неразрешимой логики, и найдены простые (по числу переменных, используемым связкам, длине) для рассматриваемых классов логик примеры неразрешимых формул.
Построена разрешимая модальная логика с неразрешимой проблемой допустимости правил вывода, что обосновывает нетривиальность задачи доказательства разрешимости проблемы допустимости правил вывода: положительное решение этой последней задачи было получено В.В.Рыбаховым для многих конкретных модальных и суперинтуиционистских логик.
Доказана неразрешимость семантического следования на конечных шкалах Кринке в различных вариантах (локальном, глобальном) и в разных классах шкал (GL-шкалы, Int-шкалы и др.). Получена также неразрешимость проблемы первопорядко-вой определимости модальных формул на классе конечных шкал9.
'Здесь и далее используются стандартизированные в [62] обозначения: (N)ExtL — класс (нормальных) расширений логики L; так, Extlnt обозначает класс су-перянтуинионистскшс логик, NExtS4 — класс нормальных расширений модальной логики S4.
'Результат получек совместно с Л.А.Чагровой; см. сноску на странице 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 наименования.
