Laboratory of Mathematical Logic at PDMI

Пятница, 14 ноября, комната 106. Начало в 19:00.

Докладчик: С. Николенко.

Тема: Ограниченная арифметика и системы доказательств резолюционного типа.

Abstract

Доклад посвящен взаимосвязи между ограниченной арифметикой (Bounded Arithmetic, арифметика Пеано с ограниченными кванторами) и системами вывода d-LK, обобщающими резолюцию (правило сечения можно применять не только к литералам, но и к формулам ограниченного размера).