Аннотация:
Динамические логики — это формальные системы для рассуждений о работе компьютерных программ. Изначально подобные системы использовались для формализации понятия корректности программы и её соответствия некоторой спецификации. Однако динамические логики могут быть также использованы для установления эквивалентности алгоритмов, автоматического синтеза программ и так далее. Помимо своей
практической применимости, динамические логики представляют исследовательский интерес как соединение идей одновременно классической логики, модальной логики и вычислимости.
В моем докладе я дам основные мотивировки, такие как само определения "программы", расскажу о языке пропозициональной динамической логики PDL, семантике этого языка и о его дедуктивной системе. Также будут
покрыты некоторые результаты об алгоритмической сложности для PDL.
