О сложности в Генценовском нормальном выводе

[alex_dorin]

Здравствуйте !
Что можно сказать о степени сложности с точки зрения выводимости предложений а Генценовском нормальном выводе ?

С уважением
Александр Дорин

[Sonic86]

alex_dorin в сообщении #752422 писал(а):

Что можно сказать о степени сложности с точки зрения выводимости предложений а Генценовском нормальном выводе ?

Что такое "сложность предложений с точки зрения выводимости в генценовском нормальном выводе"?

[alex_dorin]

Истинность выводимого предложения в Генценовских системах эквивалентна
одновременной истинности не закрытых секвенций на каждом шаге поиска
доказательства. Каждая секвенция редуцируется в предложение первопорядковой логики. Уменьшается ли сложность этого предложения, полученного указанной редукцией, относительно сложности вывода исходного предложения ?
С уважением
Александр Дорин

[Sonic86]

Sonic86 в сообщении #752590 писал(а):

Что такое "сложность предложений с точки зрения выводимости в генценовском нормальном выводе"?

Определение приводите, иначе разговор бессмысленен. В Вашем последнем посте определения нет.

[alex_dorin]

К сожалению это сложно. Привожу
Тема: «Логический и сложностной анализ проблем вычислений и теории доказательств».
Номер госрегистрации
01200852829.
Руководитель темы:
доктор физ.-матем. наук
В.П. Оревков

[Sonic86]

alex_dorin в сообщении #752783 писал(а):

К сожалению это сложно. Привожу
Тема: «Логический и сложностной анализ проблем вычислений и теории доказательств».
Номер госрегистрации
01200852829.
Руководитель темы:
доктор физ.-матем. наук
В.П. Оревков

Вы думаете, мне это что-нибудь скажет?
Не ну если Вы не знаете, о чем у Вас тема (а она о чем-то конкретно), то надо выяснить у научрука.
Если интересует асимптотика работы алгоритма генценовского вывода, то так и напишите и тогда надо алгоритмы смотреть, сколько их там.
Если же Вам надо понятие сложности самому уточнить до какого-то формально точного понятия, то я - пас, надо хотя бы знать, на что Вы или Ваш научрук хотите ориентироваться.

[nikvic]

"Предложение" может быть и невыводимым.
В случае выводимости естественно говорить о минимальной длине выводов, но столь же естественно о времени какого-то алгоритма, находящего выводы.
Первый подход тяготеет к вещам типа колмогоровской/марковксой сложности, второй - к сложности вычислений.
Быть может, ТС пояснит, что он хочет.