Нормализация термов в точных моделях логики доказательств LPстатьяИсследовательская статья
Статья опубликована в журнале из списка RSCI Web of Science
Статья опубликована в журнале из перечня ВАК
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 24 июля 2024 г.
Аннотация:Базисная модель логики свидетельств является точной, если конструкторы свидетельских термов ·,+, ! в модели интерпретируются в точности в соответствии с их неформальным пониманием как применение правила modus ponens, объединение и верификациясвидетельств. В статье строится пример точной базисной модели для логики доказательствLP и доказывается, что в точных моделях LP каждый терм эквивалентен некоторому полиному доказательств.