World Logic Day 2025 – Ukraine

В рамках 7-го Всесвітнього Дня Логіки (https://worldlogicday.com/events та https://wld.cipsh.international/wld2025.html) Українським Логічним Товариством організовано дистанційний семінар «Логіка та її Застосування».

Доповідач: Іванов Євген, к.ф.-м.н., доцент.

Тема: «Теорія абстрактних переписувальних систем, орієнтована на кібер-фізичні системи».

Дата: 14 січня 2025 року у 12:00 за київським часом.

ZOOM LINK:
https://us04web.zoom.us/j/76047859778?pwd=OHBswYSAr8Bk3iSuSGjLDGJRUbIzUa.1

Теорія переписувальних систем є частиною теоретичних основ інформатики, яка типово використовується для формального моделювання та аналізу перетворень синтаксичних об’єктів, таких як терми, але не є обмеженою такими застосуваннями. Ряд базових результатів, важливих для даної теорії (наприклад, принцип нетерової індукції для переписувальних систем, лема Ньюмана, метод спадних діаграм ван Оострома – де Брейна), можуть бути сформульовані на абстрактному рівні, що не накладає обмежень на структуру та подання елементів системи і правил переписування. Такі результати належать до змісту абстрактної теорії переписувальних систем і, здебільшого, спираються на припущення про термінальність, слабку нормалізованість та/або зліченність системи, що виконуються для абстрактних переписувальних систем, породжених дискретними моделями обчислень або логічного виводу, але не завжди виконуються для абстрактних переписувальних систем, породжених дискретно-неперервними математичними моделями, важливими для парадигми кібер-фізичних систем. У даній роботі пропонуються розширення і узагальнення класичних результатів теорії абстрактних переписувальних систем на випадки, коли такі системи не задовольняють припущенням про термінальність, слабку нормалізованість та/або зліченність, що становлять інтерес з точки зору формального моделювання та аналізу математичних моделей кібер-фізичних систем.

Результати, про які повідомляється у даній доповіді, включають: формально верифікований доказ повноти методу спадних діаграм ван Оострома – де Брейна для доведення конфлюентності абстрактних переписувальних систем мінімальної незліченної потужності, розв'язки проблем неповноти методу спадних діаграм з двома мітками та відсутності колапсу на рівні 2 ієрархії систем, що мають спадну властивість Черча – Россера, узагальнення леми Ньюмана на випадки зліченних та незліченних строго індуктивних переписувальних систем, спеціальні принципи індукції для доведення властивостей елементів переписувальних систем, що не задовольняють припущенням про термінальність та зліченність.

Ключові слова: абстрактна переписувальна система, формальне доведення, формальні методи, кібер-фізичні системи.

ВІДОМОСТІ ПРО АВТОРА

ІВАНОВ Євген
кандидат фізико-математичних наук, доцент
Київський національний університет імені Тараса Шевченка

Celebrating the 7 th World Logic Day ( https://worldlogicday.com/events and https://wld.cipsh.international/wld2025.html) Ukrainian Logic Society organizes online seminar «Logic and its Applications»

DATE: Tuesday, January 14, 2025

TIME: 12.00 (Kyiv time, EES time); 10.00 (GMT+2 )

VENUE: ZOOM, LINK
https://us04web.zoom.us/j/76047859778?pwd=OHBswYSAr8Bk3iSuSGjLDGJRUbIzUa.1

Speaker: IVANOV Ievgen
Talk title: «Abstract Rewriting Theory Oriented Towards Cyber-Physical Systems»

Rewriting theory is a part of the theoretical foundations of informatics that is typically used for formal modeling and analysis of transformations of syntactical objects like terms, but is not limited to such applications. A number of basic results important for this theory (for example, Noetherian induction principle for rewriting systems, Newman’s lemma, Van Oostrom – De Bruijn decreasing diagrams method) can be formulated on an abstract level that does not impose restrictions on the structure and representation of elements of a system and its rewrite rules. Such results belong to the abstract rewriting theory, and, they usually depend on the assumptions about termination, weak normalization and/or countability of a system that hold for abstract rewriting systems induced by discrete models of computation and logical inference, but not always hold for abstract rewriting systems induced by discrete-continuous mathematical models important for the paradigm of cyber-physical systems.

In this work we propose extensions and generalizations of classical results of the theory of abstract rewriting systems to the cases where such systems do not satisfy the assumptions about termination, weak normalization and/or countability and that are interesting from the perspective of formal modeling and analysis of mathematical models of cyber-physical systems. The results discussed in this talk include: a formally verified proof of completeness of Van Oostrom – De Bruijn decreasing diagrams method for proving confluence of abstract rewriting systems of the least uncountable cardinality, solutions of the problems of incompleteness of the decreasing diagrams method with two labels and the absence of collapse of the hierarchy of Decreasing Church-Rosser rewriting systems at the level 2, generalizations of Newman’s lemma to the cases of countable and uncountable strictly inductive rewriting systems, special induction principles for proving properties of elements of rewriting systems that do not satisfy the termination and countability assumptions.

Keywords: abstract rewriting system, formal proof, formal methods, cyber-physical systems.

INFORMATION ABOUT AUTHOR

IVANOV Ievgen
Candidate of Physical and Mathematical Sciences, Docent
Taras Shevchenko National University of Kyiv