Рус Eng За 365 дней одобрено статей: 1930,   статей на доработке: 305 отклонено статей: 746 
Библиотека
Статьи и журналы | Тарифы | Оплата | Ваш профиль

Вернуться к содержанию

R-I-Г-конструкции для логик времени
Толстухин Алексей Вадимович

аспирант, кафедра логики, философский факультет, Московский Государственный Университет имени М.В. Ломоносова

119234, Россия, Москва область, г. Москва, ул. Ленинские Горы, 1, оф. 834

Tolstukhin Aleksei

Post-graduate student, the department of Logics, M. V. Lomonosov Moscow State University

119234, Russia, Moskva oblast', g. Moscow, ul. Leninskie Gory, 1, of. 834

alexei.tolstukhin@gmail.com
Другие публикации этого автора
 

 

Аннотация.

Предметом исследования является проблема остановки вывода в модальных логиках, в частности логиках времени. Для рассмотрения выбрана логика времени с линейным транзитивным и плотным временным потоком. Одним из подходов в решении рассматриваемой проблемы является применение метода мозаик, суть которого заключается в нахождении конечного множества фрагментов, которое может быть достроено до бесконечной модели, для доказательства формулы. На основании метода мозаик возможно построение различных исчислений, например, R-I-Г-исчисления, которое сочетает в себе метод мозаик, процедуру loop-cheak и интуитивную ясность табличного исчисления. В исследовании применяется формализация в вопросе описания временного потока, а также дедуктивный метод для построения исчисления. Новизна работы заключается в представлении оригинального подхода к решению проблемы остановки вывода в логиках времени. Основываясь на идее метода мозаик, предложено исчисление R-I-Г-конструкций, которое в силу своих правил гарантировано строит конечный вывод. Дополнив систематическую процедуру правилами насыщения, можно попытаться получить насыщенное множество мозаик, которое является доказательством выполнимости формулы.

Ключевые слова: Метод мозаик, Исчисление, R-I-Г-конструкции, Логика времени, Насыщенное множество мозаик, Марк Рейнолдс, временной поток, Луп-чек, проблема остановки вывода, аналитические таблица

DOI:

10.25136/2409-8728.2018.6.26354

Дата направления в редакцию:

21-05-2018


Дата рецензирования:

21-05-2018


Дата публикации:

22-05-2018


Abstract.

The subject of this research is the problem of stopping proof in modal logics, particularly the logics of time. Form consideration, the author selected the logics of tine with the linear transitive and dense time flow. One of the approaches in solution of the task at hand lies in application of the mosaic method, which essence consists in the presence of the finite set of fragments that can be added on towards the infinite model for proving the formula. The mosaic method allows structuring various computations, for example the R-I-G computations, which combines the mosaic method, loop-check procedure, and intuitive clarity of tabular computation. The research applies formalization in terms of describing the time flow, as well as deductive method of structuring the computation. The scientific novelty consists in introduction of an original approach towards solution of the problem of stopping proof within the logics of time. Leaning on the idea of mosaic method, the author suggests the computation of R-I-G constructs, which in virtue of its rules builds the end conclusion. Having complemented the systematic procedure with the saturation rules, an attempt can be made to acquire a saturated set of mosaics that manifests as a proof for the feasibility of formula.

Keywords:

problem of stopping proof, Loop-cheak, time flows, Mark Reynolds, Saturated set of mosaics, Temporal Logic, R-I-G-constraction, Calculi, Mosaic Method, analitic tableau

Введение

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

Безусловно, кроме своего практического применения, временная логика представляет интерес и для философского рассмотрения. Многие исследователи [12] склоны считать, что время в фокус рассмотрения философов попало благодаря работе "Критика чистого разума" немецкого философа И. Канта: «На этой априорной необходимости основывается также возможность аподиктических основоположений об отношениях времени или аксиом о времени вообще. Время имеет только одно измерение: различные времена существуют не вместе, а последовательно...". Однако проблему овременненых высказываний поднимает ещё Аристотель в [1], который пытается разобраться, каким образом оценивать высказывания о событиях, которые ещё не произошли и неизвестно произойдут ли, на всем известном примере о морском сражении.

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

Проблема «остановки» является распространенной проблемой для многих модальных логик. Суть проблемы заключается в том, что при построении вывода в исчислениях для модальных логик мы сталкиваемся с бесконечностью вывода, вызванной цикличностью в отдельных ветвях вывода, а иногда и с бесконечностью самих ветвлений. Существуют различные подходы к решению этих проблем, одним из которых является процедура loop-check [4]. При этом нет единого универсального метода решения.

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

Для решения проблемы «остановки» для мы будем использовать аналитико-табличное исчисление -- -конструкций, которое является производным от -конструкций исчисления [2], которое также основано на идее мозаик.

Метод мозаик используется для доказательства полноты и разрешимости систем неклассической и фрагментов первопорядковой классической логики. Своими корнями метод уходит в область алгебраических логик. Среди первых работ, где используется данный метод, можно указать работы венгерского логика И.Немети [8]. Изначально мозаики применялись к модальным логикам, в том числе многомерным. М. Рейнолдс, работавший с последними [13], перенес метод на временные логики, адаптировав под разные системы.

С помощью мозаик доказывают полноту аксиоматизации логики линейного времени с прайоровскими модальностями и , её разрешимость, полноту аналитико-табличного формализма [7]. Кроме того данный метод позволяет исследовать вопросы, связанные с алгоритмической сложностью проблем разрешимости [15].

Метод популярен среди исследователей в силу своей относительной простоты. Его идея состоит в том, что вместо того, чтобы иметь дело с «большой» моделью для некоторой формулы, можно попытаться показать, что для построения этой модели достаточно иметь конечное множестве всех различных фрагментов модели. Из них вся модель, возможно бесконечная, воспроизводится применением пошаговой процедуры. Для доказательства разрешимости существенно, чтобы само множество этих фрагментов было разрешимым. А сами такие фрагменты именуются мозаиками .

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

В первой части статьи даны основные определения, аксиомы и семантика рассматриваемой логики .

Вторая часть посвящена -- -конструкциям и аналитическим таблицам.

В третей части работы будет рассмотрено применение -- -конструкция для доказательства выполнимости и общезначимости формулы.

1. Основные определения

Алфавит языка , в котором построено исчисление -- -конст- рукций, состоит из счетно-бесконечного числа пропозициональных связок {, ,}, переменных {}, операторов {}, модального оператора (необходимости) и технических символов {(,)}. Оператор будем определять как , где - формула языка

Формулами языка являются пропозициональные переменные и выражения вида , , , , , , , , где и - формулы языка . Далее заглавными буквами латинского алфавита (, , и т.д.) будем обозначать произвольные формулы, а заглавными буквами греческого алфавита (, и т.д.) - множества формул.

содержит следующий перечень аксиом:

Пропозициональная связка определяется стандартно через и .

Правила системы :

Семантическими структурами являются структуры Крипке (), где - непустое множество, а - бинарное отношение на множестве , которое обладает следующими свойствами:

1. (свойство антирефлексивности);

2. (свойство асимметричности);

3. (свойство транзитивности);

4. (свойство линейности).

Определение 1 Модельной структурой (моделью) называем кортеж , в котором:

1. ;

2. есть отношение на ;

3. есть функция оценки.

Истинность формулы в модели определяется следующим образом: , для каждой пропозициональной переменной и формул и :

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

Определение 2 Пара и функция : образуют мозаику c базой { }, если для любой формулы из и для каждого выполняются следующие условия:

Если база мозаики является одноэлементным множеством, то данная мозаика называется вырожденной .

Определение 3 Множество M называется насыщенным множеством мозаик, если для всякой мозаики верны следующие утверждения:

1. Если и , то существует такая мозаика , что , и ;

3. Если и , то существует такая мозаика , что , и .

Всякое множество состоящее только из вырожденной мозаики, является насыщенным.

Таким образом, основной леммой является следующее утверждение.

Лемма 1 Формула выполняется в тогда и только тогда, когда существует согласованное насыщенное множество мозаик для .

Для доказательства данной леммы достаточно доказать два утверждения:

Утверждение 1 Если формула выполняется в , то существует согласованное множество мозаик .

Утверждение 2 Если существует насыщенное множество мозаик для формулы , то выполним в некоторой модели .

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

2. Аналитические таблицы

Для работы с методом мозаик во временной логике удобно использовать подход, который позволяет сразу фиксировать множество пар, образующих базу мозаики, и результат применения правил редукции. Подобный подход --конструкций был предложен О.М. Григорьевым. - это множество пар префиксов, которыми обозначены формулы, а - множество индексированных формул. Позже по предложению Григорьева --конструкции были дополнены множеством , роль которого заключалась в фиксации суффиксов формул с модальностями и , которые приводят к циклам при построении аналитической таблицы. Таким образом, получаются -- -конструкции.

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

Определение 4 Индексированная формула есть пара , или просто , где есть целое положительное число, а - формула языка .

Множество из -- -конструкции отвечает за фиксирование отношения достижимости между мирами, так как с каждой индексированной формулой ассоциированны пары индексов. Также будем производить пересчет всех временных операторов и в формуле, которую подаем на вход в аналитическую таблицу. Например, пусть дана формула . Присваивая каждому оператору и свой номер, получаем . Для учета этих операторных индексов в элементарную -- -конструкцию вводится ещё одно множество .

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

-- -конструкцию для удобства будем записывать в виде .

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

Традиционно правила редукции будем записывать в виде дроби:

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

Определение 7 L -аналитико-табличное исчисление есть конечная совокупность правил редукции ,..., .

Пусть имеется конечная последовательность -- -конструкций , ,..., ().

Определение 8 Последовательность , ,..., , ,..., получена из последовательности , ,..., применением правила , если совпадает с посылкой правила , а ,..., - с его заключением.

Представим -аналитико-табличное исчисление.

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

Используем стандартное определение дерева с корнем.

Определение 9 Пусть - конечное дерево - - -конструкций и получено из применением правила .

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

Определение 10

1. Любая отдельно взятая -- -конструкция есть -дерево.

2. Если есть -дерево и есть -дерево.

3. Ни что иное не является -деревом.

Определение 11 -аналитическая таблица для формулы языка - конечное -дерево, корень которого есть - - -конс- трукция вида .

Определение 12 - - -конструкция замкнута в случае, если для некоторых и : . Ветвь -аналитической таблицы замкнута, если последняя - - -конструкция в этой ветви замкнута. -аналитическая таблица замкнута, если все её ветви замкнуты. Формула языка называется -совместной, если не существует замкнутой аналитической таблицы для . Формула языка есть теорема -аналитико-табличного исчисления, если не существует замкнутой -аналитической таблицы для .

Определение 13 Ветвь -аналитической таблицы закончена в том случае, если к последней её - - -конструкции не применимо ни одно правило -аналитико-табличного исчисления. -анали- тическая таблица закончена, если закончены все её незамкнутые ветви. -аналитическая закончена, если закончена всякая её ветвь.

3. Построение аналитико-табличного вывода на основе -- -конструкций

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

Рассмотрим процедуру построения -- -конструкции для формулы .

Больше никаких правил редукции применить невозможно. Правила, которые бы преобразовали множество , также нельзя применить, так как множество содержит в себе пару , которая может получиться в результате применения правила .

Теперь можно приступить к подробному рассмотрению множества . Определим функцию следующим образом: каждому элементу пар из множества сопоставляется множество формул с этим индексом, то есть

где формула с индексом - индексированная формула.

В результате получается следующий набор множеств.

Рассмотрим первую пару из множества (1,2). Для удобства будем называть пары из множества протомозаиками. Является ли протомозаика () мозаикой?

Согласно определению мозаики для пары (1,2) должно выполняться следующее условие: . В связи с этим дополним множество формулой . Остальные условия из определения выполняются.

Аналогично достраиваем протомозаику (2,3) до мозаики добавлением формулы в множество .

Таким образом, множество протомозаик является множеством мозаик. Следующим шагом является проверка, является ли данное множество насыщенным множеством мозаик?

За не имением в формуле модальности нам необходимо проверить только первые два условия из определения множества мозаик.

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

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

Пусть такой мозаикой будет :

Таким образом, возникает противоречие. Мозаика не соответствует третьему условию из определения мозаики. Исправить это возможно дополнением множества формулами и , последняя из которых приводит к возникновению нового дефекта будущего. Так можно продолжать до бесконечности.

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

Определение 14 - - -конструкция называется вниз насыщенной относительно правил нашего исчисления, если выполняются следующие условия:

1. не замкнута,

2. ,

3. и ,

4. или ,

5. для всех таких, что ,

6. для всех таких, что ,

7. существует такой, что и для некоторого ,

8. существует такой, что и для некоторого ,

9. ,

10. или или для некоторого ,

11. или или для некоторого .

Для вниз насыщенным мозаик существует следущие леммы.

Лемма 2 Если есть незамкнутая насыщенная аналитическая таблица для формулы языка , то существует вниз насыщенная - - -конструкция

Лемма 3 Пусть есть вниз насыщенная - - -конструкция. Тогда существует насыщенное множество мозаик .

Таким образом, формула, которая была рассмотрена выше явлется выполнимой, так как её аналитическая таблица незамкнута. По Лемме 2 мы можем получить вниз насыщенную -- -конструкцию для нее. Следовательно, по лемме 3, формула является выполнимой. Доказательства лемм в силу громоздкости в данной статье опущены.

Заключение

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

Возникает резонный вопрос, а можно ли построить исчисление таким образом, чтобы полученное множество уже являлось необходимым насыщенным множеством мозаик. Возможный ответ заключается в построении -- -исчисления аналогичного тому, что представлено в работе Рейнолдса, Маркса и Микуласа [7].

Библиография
1.
Аристотель. Об истолковании. Соч., т. 2, гл. 9. М., 1978
2.
Григорьев О. М. Аналитико-табличная формализация систем временной логики. Кандидатская диссертация. Москва. 2004.
3.
Bian J., French T., Reynolds M. An Efficient Tableau for Linear Time Temporal Logic. // AI 2013: Advances in Artificial Intelligence, p. 289-300, 2013.
4.
Heuerding A., Seyfried M., Zimmermann H. Effecient loop-check for backward proof search in some non-classical propositional logics.//Proc. 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX’96), Lecture Notes in Artificial Intelligence, Vol. 1071, Springer, Berlin, 1996, pp. 210–225
5.
Indrzejzak А. Natural Deduction, Hybrid Systems and Modal Logics. In R.Wojcicki, V.Hendricks, D. Mundici, E. Orlowska, K. Segerberg, H. Wansing, editors//Trends in Logic, v. 30, p. 332-362. Springer, 2010.
6.
Leszczynska D. A Loop-Free Decision Procedure for Modal Propositional Logics K4, S4 and S5. Journal of Philosophical Logic, 38:151-177, 2009.
7.
Marx M., Mikul'{а}s S., and Reynolds M. The mosaic method for temporal logics.//Dyckhoff R.,editor, Automated Reasoning with Analytic Tableaux and Related Methods. Proceeding of International Conference, TABLEAUX 2000. LNAI 1947. Springer, 2000. P.324-340.
8.
Nemeti I. Decidable versions of first order logic and cylindric-relativized set algebras.// Csirmaz L., Gabbay D.M., and de Rijke M., editors, Logic Coloquium '92. CSLI Publications. 1995. P.171-241.
9.
Nemeti I. Free Algebras and Decidability in Algebraic Logic. PhD thesis. Hungarian Academy of Sciences, Budapest. 1986
10.
Prior A. N. Time and modality. Oxford University Press, Oxford, 1957
11.
Prior A. N. Past, present, and future. Clarendon Press, Oxford, 1967
12.
Rescher N., Urquhart A. Temporal logic // Springer, 1971
13.
Reynolds M. A decidable logic of parallelism. // Notre Dame Journal of Formal Logic. 1997. V. 38. P. 419-436.
14.
Reynolds M. The complexity of the temporal logic with until over general linear time. // Journal of Computer and System Science. 2003. V. 66. P. 393-426
15.
Reynolds M. The complexity of temporal logic over the reals. Annals of Pure and Applied Logic. Vol. 161, Issue 8, May 2010, P. 1063-109
References (transliterated)
1.
Aristotel'. Ob istolkovanii. Soch., t. 2, gl. 9. M., 1978
2.
Grigor'ev O. M. Analitiko-tablichnaya formalizatsiya sistem vremennoi logiki. Kandidatskaya dissertatsiya. Moskva. 2004.
3.
Bian J., French T., Reynolds M. An Efficient Tableau for Linear Time Temporal Logic. // AI 2013: Advances in Artificial Intelligence, p. 289-300, 2013.
4.
Heuerding A., Seyfried M., Zimmermann H. Effecient loop-check for backward proof search in some non-classical propositional logics.//Proc. 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX’96), Lecture Notes in Artificial Intelligence, Vol. 1071, Springer, Berlin, 1996, pp. 210–225
5.
Indrzejzak A. Natural Deduction, Hybrid Systems and Modal Logics. In R.Wojcicki, V.Hendricks, D. Mundici, E. Orlowska, K. Segerberg, H. Wansing, editors//Trends in Logic, v. 30, p. 332-362. Springer, 2010.
6.
Leszczynska D. A Loop-Free Decision Procedure for Modal Propositional Logics K4, S4 and S5. Journal of Philosophical Logic, 38:151-177, 2009.
7.
Marx M., Mikul'{a}s S., and Reynolds M. The mosaic method for temporal logics.//Dyckhoff R.,editor, Automated Reasoning with Analytic Tableaux and Related Methods. Proceeding of International Conference, TABLEAUX 2000. LNAI 1947. Springer, 2000. P.324-340.
8.
Nemeti I. Decidable versions of first order logic and cylindric-relativized set algebras.// Csirmaz L., Gabbay D.M., and de Rijke M., editors, Logic Coloquium '92. CSLI Publications. 1995. P.171-241.
9.
Nemeti I. Free Algebras and Decidability in Algebraic Logic. PhD thesis. Hungarian Academy of Sciences, Budapest. 1986
10.
Prior A. N. Time and modality. Oxford University Press, Oxford, 1957
11.
Prior A. N. Past, present, and future. Clarendon Press, Oxford, 1967
12.
Rescher N., Urquhart A. Temporal logic // Springer, 1971
13.
Reynolds M. A decidable logic of parallelism. // Notre Dame Journal of Formal Logic. 1997. V. 38. P. 419-436.
14.
Reynolds M. The complexity of the temporal logic with until over general linear time. // Journal of Computer and System Science. 2003. V. 66. P. 393-426
15.
Reynolds M. The complexity of temporal logic over the reals. Annals of Pure and Applied Logic. Vol. 161, Issue 8, May 2010, P. 1063-109