Іванов Є. В. Узагальнена теорiя абстрактних переписувальних систем

English version

Дисертація на здобуття ступеня доктора наук

Державний реєстраційний номер

0526U000115

Облікова картка дисертації

0526U000115.pdf

Здобувач

Спеціальність

  • 01.05.01 - Теоретичні основи інформатики та кібернетики

28-05-2026

Спеціалізована вчена рада

Д 26.001.09

Київський національний університет імені Тараса Шевченка

Анотація

Робота присвячена побудовi теорiї, що розширює та узагальнює класичнi результати теорiї абстрактних переписувальних систем (АПС) на випадки, що становлять iнтерес з точки зору аналiзу недискретних математичних моделей систем i процесiв. Однiєю з центральних тем класичної теорiї АПС є дослiдження властивостi Черча-Россера (або еквiвалентної властивостi конфлюентностi), що виражає зв’язок мiж вiдношеннями конверсiї та редукцiї та має як наслiдок властивiсть iснування не бiльше однiєї нормальної форми у кожного елемента системи. Методи перевiрки властивостi Черча-Россера (конфлюентностi) дослiджувалися протягом тривалого перiоду 20-го столiття та на початку 21-го столiття Тепер такi методи є добре вивченими для систем, що мають спецiальнi властивостi, характернi для дискретних моделей обчислень, такi як термiнальнiсть або злiченнiсть. Подiбна ситуацiя має мiсце i для iнших результатiв теорiї АПС. Однак, визначення застосовностi деяких iз зазначених методiв, вiдомих для злiченних або термiнальних систем, до незлiченних нетермiнальних систем вважається деякими провiдними дослiдниками з теорiї переписувальних систем важливою i фундаментальною вiдкритою проблемою. Крiм того, властивостi, такi, як термiнальнiсть i злiченнiсть не є характерними для АПС, що породженi моделями, що, в певному сенсi, поєднують недискретнiсть i недетермiнiзм, якi є важливими для сучасних мiждисциплiнарних напрямкiв, пов’язаних з iнформатикою. У зв’язку з вищезазначеним, для теоретичних основ iнформатики є актуальною побудова узагальненої теорiї АПС, що розширює та узагальнює класичнi результати теорiї АПС на випадки, що становлять iнтерес з точки зору аналiзу недискретних математичних моделей.

Читати повністю

Публікації

Ivanov I. Completeness of the decreasing diagrams method for proving confluence of rewriting systems of the least uncountable cardinality. Leibniz international proceedings in informatics. ISSN 1868-8969. 2025. Vol. 337. P. 25:1–25:20.

Ivanov I. On the cofinality property in the context of the hierarchy of decreasing Church-Rosser abstract rewriting systems. CEUR workshop proceedings. ISSN 1613-0073. 2024. Vol. 3909. P. 466–479.

Ivanov I. On Newman’s lemma and non-termination. CEUR workshop proceedings. ISSN 1613-0073. 2023. Vol. 3624. P. 14–24.

Ivanov I. Generalized Newman’s lemma for discrete and continuous systems. Leibniz international proceedings in informatics. ISSN 1868-8969. 2023. Vol. 260. P. 9:1–9:17.

Ivanov I. On induction principles for partial orders. Logica Universalis. ISSN 1661-8297. 2022. Vol. 16. P. 105–147.

Ivanov I. On Induction Principles for Diamond-Free Partial Orders. Communications in computer and information science. ISSN 1865-0929. 2021. Vol. 1308. P. 166–190.

Ivanov I. On induction for diamond-free directed complete partial orders. CEUR workshop proceedings. ISSN 1613-0073. 2020. Vol. 2732. P. 70–73.

Ivanov I., Nikitchenko M. Expressibility in the Kleene algebra of partial predicates with the complement composition. Communications in computer and information science. ISSN 1865-0929. 2020. Vol. 1175. P. 50–67.

Ivanov I., Nikitchenko M. Inference rules for the partial Floyd-Hoare logic based on composition of predicate complement. Communications in computer and information science. ISSN 1865-0929. 2019. Vol. 1007. P. 71–88.

Ivanov I., Nikitchenko M. On the Kleene algebra of partial predicates with predicate complement. CEUR workshop proceedings. ISSN 1613-0073. 2019. Vol. 2393. P. 542–551.

Ivanov I., Kornilowicz A., Nikitchenko M. An inference system of an extension of Floyd-Hoare logic for partial predicates. Formalized mathematics. ISSN 1426- 2630. 2018. Vol. 26, no. 2. P. 159–164.

Kornilowicz A., Ivanov I., Nikitchenko M. Kleene algebra of partial predicates. Formalized mathematics. ISSN 1426-2630. 2018. Vol. 26, no. 1. P. 11–20.

Ivanov I., Kornilowicz A., Nikitchenko M. Implementation of the compositionnominative approach to program formalization in Mizar. Computer science journal of Moldova. ISSN 1561-4042. 2018. Vol. 26, no.1 (76). P. 59–76.

Nikitchenko M., Ivanov I., Kornilowicz A., Kryvolap A. Extended Floyd-Hoare logic over relational nominative data. Communications in computer and information science. ISSN 1865-0929. 2018. Vol. 826. P. 41–64.

Ivanov I., Nikitchenko M. On the sequence rule for the Floyd-Hoare logic with partial pre- and post-conditions. CEUR workshop proceedings. ISSN 1613-0073. 2018. Vol. 2104. P. 716–724.

Ivanov I. On the underapproximation of reach sets of abstract continuous-time systems. Electronic Proceedings in Theoretical Computer Science. ISSN 2075- 2180. 2017. Vol. 247. P. 46–51.

Ivanov I., Nikitchenko M., Kryvolap A., Kornilowicz A. Simple-named complex-valued nominative data – definition and basic operations. Formalized Mathematics. ISSN 1426-2630. 2017. Vol. 25, no. 3. P. 205–216.

Kornilowicz A., Kryvolap A., Nikitchenko M., Ivanov I. An approach to formalization of an extension of Floyd-Hoare logic. CEUR workshop proceedings. ISSN 1613-0073. 2017. Vol. 1844. P. 504–523.

Ivanov I., Nikitchenko M., Skobelev V.G. Proving properties of programs on hierarchical nominative data. Computer science journal of Moldova. ISSN 1561- 4042. 2016. Vol. 24, no. 3 (72). P. 371-398.

Ivanov I. On local characterization of global timed bisimulation for abstract continuous-time systems. Lecture notes in computer science. ISSN 0302-9743. 2016. Vol. 9608. P. 216–234.

Ivanov I., Nikitchenko M., Abraham U. On a decidable formal theory for abstract continuous-time dynamical systems. Communications in computer and information science. ISSN 1865-0929. 2014. Vol. 469. P. 78–99.

Ivanov I. On non-triviality of the hierarchy of decreasing Church-Rosser abstract rewriting systems. Proceedings of the 13th International Workshop on Confluence. July 9, 2024, Tallinn, Estonia. P. 30-35.

Ivanov I. On confluence criteria for non-terminating abstract rewriting systems. Proceedings of the 12th International Workshop on Confluence. August 23-24, 2023, Obergurgl, Austria. P. 9-13.

Ivanov I. On generalizations of real induction. Conference on Mathematical Foundations of Informatics. Proceedings MFOI-2020. 12-16 January 2021, Kyiv, Ukraine. P. 162-167.

Ivanov I. On generalized well-founded induction. Logic and its Applications. 2nd World Logic Day – January 14, 2020. Logic and its Applications, The workshop. Book of Abstracts. January 14, 2020, Kyiv. P. 7-8.

Ivanov I. On the partial Floyd-Hoare logic based on predicate complement. 1st World Logic Day – January 14, 2019. Logic and its Applications, The workshop. Book of Abstracts. January 14, 2019, Kyiv. P. 4-5.

Ivanov E.V. On inductive definitions on non-well-ordered domains and their potential applications to verification of cyber-physical systems. Прикладнi системи та технологiї в iнформацiйному суспiльствi : зб. тез доповiдей i наук. повiдомл. учасникiв II Мiжнародної науково-практичної конференцiї. Київ, 1 жовтня 2018. С. 67-68.

Kornilowicz A., Kryvolap A., Nikitchenko M., Ivanov I. Formalization of the algebra of nominative data in Mizar. Proceedings of the 2017 Federated Conference on Computer Science and Information Systems. September 3-6, 2017, Prague, Czech Republic. P. 237-244.

Ivanov I., Nikitchenko M., Skobelev V.G. Properties of nominative programs specified by effective definitional schemes. Conference on Mathematical Foundations of Informatics. Proceedings MFOI-2016. Institute of Mathematics and Computer Science, July 25-30, 2016, Chisinau, Moldova. P. 222-240.

Ivanov I., Kornilowicz A., Nikitchenko M.S. Formalization of nominative data in Mizar. Працi Мiжнародної науково-практичної конференцiї “Теоретичнi та прикладнi аспекти побудови програмних систем” TAAPSD’2015, 23-26 листопада 2015 р., м. Київ. С. 82-85.

Ivanov Ie.V., Nikitchenko M.S. On nominative Glushkov algebras. Матерiали Всеукраїнської науково-практичної конференцiї “В.М. Глушков – пiонер кiбернетики”. 11 грудня 2014, м. Київ. С. 48-49.

Ivanov I. Completeness of decreasing diagrams for the least uncountable cardinality. Archive of Formal Proofs. ISSN 2150-914X. 2025. April. 319 pages.

Читати повністю

Файли

Dissertation_Ivanov.pdf

autoreferat-Referat_Ivanov.pdf

Схожі дисертації

0421U102388

Насіров Еміл Мехдієвич

Паралелізація невід’ємної факторизації розріджених лінгвістичних матриць та тензорів надвеликої розмірності

0420U102355

Дудар Вячеслав Вячеславович

Оптимiзацiйнi алгоритми навчання та iнварiантнiсть до геометричних перетворень нейронних мереж

0520U101700

Притоманова Ольга Михайлівна

Нечіткі задачі оптимального розбиття множин: теоретичні основи, методи та алгоритми розв’язання

0520U100242

Завадський Ігор Олександрович

Подільні коди та їх застосування

0520U100209

Рисцов Ігор Костянтинович

Застосування методів алгебраїчної теорії автоматів до проблем аналізу дискретних динамічних систем.