Normalization of Terms in Sharp Models of Logic of Proofs LPстатья
Информация о цитировании статьи получена из
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 10 апреля 2024 г.
Аннотация:Базисная модель логики свидетельств является точной, если конструкторы свидетельских термов *, +, ! в модели интерпретируются в точности в соответствии с их неформальным пониманием как применение правила modus ponens, объединение и верификация доказательств. В работе построен пример точной модели логики доказательств LP и доказано, что в точных моделях логики LP каждый терм эквивалентен некоторому полиному доказательств.