МОДЕЛИРОВАНИЕ АРИФМЕТИКИ В ЯЗЫКЕ ПЕРВОГО
ПОРЯДКА, ОБОГАЩЕННОМ ТЕМПОРАЛЬНЫМИ
КВАНТОРАМИ

Котикова, Е.А.; Рыбаков, М.Н.

МОДЕЛИРОВАНИЕ АРИФМЕТИКИ В ЯЗЫКЕ ПЕРВОГО ПОРЯДКА, ОБОГАЩЕННОМ ТЕМПОРАЛЬНЫМИ КВАНТОРАМИ

Дата публикации: 2016

Дата публикации в реестре: 2020-03-18T12:53:36Z

Аннотация:

Рассматривается язык классической логики предикатов с равенством, обогащенный модальностями темпоральной логики CTL* . В качестве семантики для него предлагаются серийные шкалы Крипке с постоянными предметными областями. Строится погружение множества арифметических формул, истинных в стандартной модели арифметики, во множество всех модальных предикатных формул, истинных в указанном классе шкал Крипке. Извлекается ряд следствий, касающихся алгоритмических, синтаксических и семантических свойств большого класса логик в рассматриваемом языке

Ключевые слова:
510.52 Сложность алгоритмов, 510.64 Неклассические, формальные логические системы

Тип: Статья