Толстухин А.В. —
R-I-Г-конструкции для логик времени
// Философская мысль. – 2018. – № 6.
– С. 23 - 32.
DOI: 10.25136/2409-8728.2018.6.26354
URL: https://e-notabene.ru/fr/article_26354.html
Читать статью
Аннотация: Предметом исследования является проблема остановки вывода в модальных логиках, в частности логиках времени. Для рассмотрения выбрана логика времени с линейным транзитивным и плотным временным потоком. Одним из подходов в решении рассматриваемой проблемы является применение метода мозаик, суть которого заключается в нахождении конечного множества фрагментов, которое может быть достроено до бесконечной модели, для доказательства формулы. На основании метода мозаик возможно построение различных исчислений, например, R-I-Г-исчисления, которое сочетает в себе метод мозаик, процедуру loop-cheak и интуитивную ясность табличного исчисления. В исследовании применяется формализация в вопросе описания временного потока, а также дедуктивный метод для построения исчисления. Новизна работы заключается в представлении оригинального подхода к решению проблемы остановки вывода в логиках времени. Основываясь на идее метода мозаик, предложено исчисление R-I-Г-конструкций, которое в силу своих правил гарантировано строит конечный вывод. Дополнив систематическую процедуру правилами насыщения, можно попытаться получить насыщенное множество мозаик, которое является доказательством выполнимости формулы.
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.