Laboratory of Mathematical Logic at PDMI

Вторник, 21 ноября, комната 106. Начало в 12:00.

Докладчик: Б. Конев.

АВТОМАТИЧЕСКОЕ ПОРОЖДЕНИЕ ДОКАЗАТЕЛЬСТВ В СЕКВЕНЦИАЛЬНЫХ ИСЧИСЛЕНИЯХ С РАВЕНСТВОМ
впервые процедура поиска вывода в секвенциальном исчислении с равенством была предложена с. кангером в середине 50-х гг. однако, в отличие от метода резолюции, до сих пор не известен способ поиска доказательств в подобных исчислениях, который давал бы приемлемую производительность. будет сделан доклад на основе обзора А. Дегтярева и А. Воронкова "equality reasoning in sequent-based calculi", представляющий различные способы поиска секвенциальных доказательств с равенством.