Правильная ссылка на статью:
Толстухин А.В..
R-I-Г-конструкции для логик времени
// Философская мысль. – 2018. – № 6.
– С. 23-32.
DOI: 10.25136/2409-8728.2018.6.26354.
DOI: 10.25136/2409-8728.2018.6.26354
Читать статью
Аннотация: Предметом исследования является проблема остановки вывода в модальных логиках, в частности логиках времени. Для рассмотрения выбрана логика времени с линейным транзитивным и плотным временным потоком. Одним из подходов в решении рассматриваемой проблемы является применение метода мозаик, суть которого заключается в нахождении конечного множества фрагментов, которое может быть достроено до бесконечной модели, для доказательства формулы. На основании метода мозаик возможно построение различных исчислений, например, R-I-Г-исчисления, которое сочетает в себе метод мозаик, процедуру loop-cheak и интуитивную ясность табличного исчисления. В исследовании применяется формализация в вопросе описания временного потока, а также дедуктивный метод для построения исчисления. Новизна работы заключается в представлении оригинального подхода к решению проблемы остановки вывода в логиках времени. Основываясь на идее метода мозаик, предложено исчисление R-I-Г-конструкций, которое в силу своих правил гарантировано строит конечный вывод. Дополнив систематическую процедуру правилами насыщения, можно попытаться получить насыщенное множество мозаик, которое является доказательством выполнимости формулы.
Ключевые слова: Метод мозаик, Исчисление, R-I-Г-конструкции, Логика времени, Насыщенное множество мозаик, Марк Рейнолдс, временной поток, Луп-чек, проблема остановки вывода, аналитические таблица
Библиография:
Аристотель. Об истолковании. Соч., т. 2, гл. 9. М., 1978
Григорьев О. М. Аналитико-табличная формализация систем временной логики. Кандидатская диссертация. Москва. 2004.
Bian J., French T., Reynolds M. An Efficient Tableau for Linear Time Temporal Logic. // AI 2013: Advances in Artificial Intelligence, p. 289-300, 2013.
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
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.
Leszczynska D. A Loop-Free Decision Procedure for Modal Propositional Logics K4, S4 and S5. Journal of Philosophical Logic, 38:151-177, 2009.
Marx M., Mikul'{а