Laboratory of Mathematical Logic at PDMI

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

2 ноября.
В.Жижкун "Разрешимые частные случаи задачи квазиунификации".
АБСТРАКТ
Задача квазиунификации возникает естественным образом в теории логического вывода при при изучении возможности обобщения доказательств (гипотеза Крайзеля). В общей постановке задача оказывается алгоритмически неразрешимой. В докладе будет приведен общий (естественно, неполный) алгоритм ее решения, а также полные алгоритмы для двух частных случаев, имеющих конкретное применение в теории вывода. Эти алгоритмы позволяют получить верхние оценки высоты термов в решении.