Вторник 28.10. В.П. Оревков: "Слабая форма свойства подформульности секвенциальных доказательств с сечениями."

Вторник, 28 октября, Zoom. Начало в 14:00.

Докладчик: В.П. Оревков (ПОМИ).

Тема: Слабая форма свойства подформульности секвенциальных доказательств с сечениями..

Abstract

В докладе будут сформулированы условия, когда правила, которые
применяются в доказательствах с сечениями, не будут применяться
после устранения сечений. Будет также доказана индукцией по глубине
формул теорема об устранимости сечений в классическом исчислении
предикатов.