Reference:
Tolstukhin A..
R-I-G constructs for the logics of time
// Philosophical Thought. – 2018. – ¹ 6.
– P. 23-32.
DOI: 10.25136/2409-8728.2018.6.26354.
DOI: 10.25136/2409-8728.2018.6.26354
Read the article
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
References:
Aristotel'. Ob istolkovanii. Soch., t. 2, gl. 9. M., 1978
Grigor'ev O. M. Analitiko-tablichnaya formalizatsiya sistem vremennoy logiki. Kandidatskaya dissertatsiya. Moskva. 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 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.
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'{a