Вторник, 28 октября, Zoom. Начало в 14:00.
Докладчик: В.П. Оревков (ПОМИ).
Тема: Слабая форма свойства подформульности секвенциальных доказательств с сечениями..
Abstract
В докладе будут сформулированы условия, когда правила, которые
применяются в доказательствах с сечениями, не будут применяться
после устранения сечений. Будет также доказана индукцией по глубине
формул теорема об устранимости сечений в классическом исчислении
предикатов.