Аннотация: Предметом исследования являются логики с линейным потоком времени. На данный момент данный системы представляют собой интерес не только с точки зрения философии, но также имеют практическое применение в области информатики. Для этих обеих областей знаний важным является вопрос о доказательстве формул в системе, то есть наличия разрешающей процедуры. С начала XXI века одним из подходов к проблеме разрешимости временной логики является процедура пошагового построения модели для формулы, которая осуществляется по принципу мозаик, маленьких фрагментов большой модели, которые выступают "строительными элементами" возможно бесконечной модели. В работе проводится анализ и подробный разбор последних исследований, посвященных данной проблематике и их систематизация. Особым вкладом автора можно считать тот факт, что до сих пор не проводилось подобного разбора на русском языке. В работе не только представлена идея метода мозаик, но также продемонстрированы ключевые леммы, доказывающие эффективность данного подхода. Следующим этапом можно считать построение исчисления, которое было бы основано на идее мозаик, доказательство его непротиворечивости и полноты.

Abstract: The subject of this research is logics with the linear flow of time. Currently, such system are represent interest not only from the philosophical perspective, but also have practical application in the field of informatics. For both of the indicated areas of knowledge, relevant is the question of proof of formulas in the system, in other words, presents of the decision procedure. Since the early XXI century, one of the approaches towards the problem of decidability of the temporal logics is the procedure of recursive structuring of the model for a formula, which is realizes in accordance with the mosaic principle, small fragments of large model that manifest as “construction” elements” of a supposedly infinite model. The work conducts a detailed analysis of the recent case studies dedicated to this problematic, as well as their systematization. The author is the first to perform a detailed analysis in the Russian language. The article presents not only the idea of mosaic method, but also demonstrates the key lemmas proving the effectiveness of this approach. The next step can be considered the development of calculation based on the mosaic method, proof of its consistency and completeness.