Laboratory of Mathematical Logic at PDMI

Пятница, 20 апреля, комната 106. Начало в 17:00.

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

МЕТОДЫ ПОИСКА ДОКАЗАТЕЛЬСТВ ДЛЯ СКУЛЕМОВСКОГО ФРАГМЕНТА ИСЧИСЛЕНИЯ ПРЕДИКАТОВ
Предваренная формула исчисления предикатов находится в скулемовской форме, если в ее префиксе кванторы существования предшествуют кванторам всеобщности. В докладе будут рассмотрены: 1) варианты сведения формул к скулемовскому виду; 2) методы элиминации функциональных знаков; 3) метод резолюций и обратный метод для скулемовского случая; 4) разрешимые подклассы исчисления предикатов.