|
Записки научных семинаров ПОМИ, 2001, том 277, страницы 80–103
(Mi znsl1430)
|
|
|
|
Эта публикация цитируется в 1 научной статье (всего в 1 статье)
Верхняя оценка высоты термов в выводах с сечениями по формулам ограниченной глубины связанных вхождений
Б. Ю. Конев Санкт-Петербургское отделение Математического института им. В. А. Стеклова РАН
Аннотация:
Доказана верхняя оценка высоты термов, входящих в наиболее общий унификатор, для случая, когда множество неизвестных разбивается на два класса. Неизвестная принадлежит к первому классу, если глубины всех ее вхождений совпадают; мы называем такую неизвестную неизвестной типа сечения. Неизвестные второго типа (неизвестные не типа сечения) могут иметь вхождения произвольной глубины. Мы оцениваем сверху высоту термов в наиболее общем унификаторе в терминах количества неизвестных не типа сечения и высоты задачи унификации. Из данной оценки вытекает верхняя оценка размера термов, входящих в доказательства в секвенциальном исчислении с сечениями, при условии, что глубина связанных вхождений переменных в формулы сечения ограничена. Библ. – 18 назв.
Поступило: 29.08.2000
Образец цитирования:
Б. Ю. Конев, “Верхняя оценка высоты термов в выводах с сечениями по формулам ограниченной глубины связанных вхождений”, Теория сложности вычислений. VI, Зап. научн. сем. ПОМИ, 277, ПОМИ, СПб., 2001, 80–103; J. Math. Sci. (N. Y.), 118:2 (2003), 4982–4993
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/znsl1430 https://www.mathnet.ru/rus/znsl/v277/p80
|
|