|
Труды ордена Ленина Математического института имени В. А. Стеклова, 1972, том 121, страницы 14–56
(Mi tm3110)
|
|
|
|
Обратный метод и тактики установления выводимости для исчисления с функциональными знаками
С. Ю. Маслов
Аннотация:
Подробно излагается конкретизация обратного метода (РЖМат, 1969, 2А100), позволяющая
устанавливать выводимость в классическом исчислении предикатов (для исходных
формул произвольной структуры). Доказаны теоремы полноты ряда тактик (в различных
сочетаниях), что позволяет жестко регламентировать переборы в процессе установления
выводимости; особое внимание уделено тактикам, основанным на унификации порядка членов
в благоприятных наборах. Установлена связь между сложностями обоснования благоприятности
и генценовского вывода (за сложность последнего принимается число применений
$\exists$-правил).
Библ. 24 назв.
Образец цитирования:
С. Ю. Маслов, “Обратный метод и тактики установления выводимости для исчисления с функциональными знаками”, Логические и логико-математические исчисления. 2, Тр. МИАН СССР, 121, 1972, 14–56; Proc. Steklov Inst. Math., 121 (1972), 11–60
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/tm3110 https://www.mathnet.ru/rus/tm/v121/p14
|
|