Eng During last 365 days Approved articles: 2088,   Articles in work: 309 Declined articles: 853 
Articles and journals | Tariffs | Payments | Your profile

Back to contents

R-I-G constructs for the logics of time
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





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



Article was received:


Review date:


Publish date:


This article written in Russian. You can find full text of article in Russian here .

Aristotel'. Ob istolkovanii. Soch., t. 2, gl. 9. M., 1978
Grigor'ev O. M. Analitiko-tablichnaya formalizatsiya sistem vremennoi 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 (TABLEAUX96), Lecture Notes in Artificial Intelligence, Vol. 1071, Springer, Berlin, 1996, pp. 210225
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}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.
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.
Nemeti I. Free Algebras and Decidability in Algebraic Logic. PhD thesis. Hungarian Academy of Sciences, Budapest. 1986
Prior A. N. Time and modality. Oxford University Press, Oxford, 1957
Prior A. N. Past, present, and future. Clarendon Press, Oxford, 1967
Rescher N., Urquhart A. Temporal logic // Springer, 1971
Reynolds M. A decidable logic of parallelism. // Notre Dame Journal of Formal Logic. 1997. V. 38. P. 419-436.
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
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