2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




 
 О сложности в Генценовском нормальном выводе
Сообщение06.08.2013, 09:31 
Здравствуйте !
Что можно сказать о степени сложности с точки зрения выводимости предложений а Генценовском нормальном выводе ?

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

 
 
 
 Re: О сложности в Генценовском нормальном выводе
Сообщение06.08.2013, 18:04 
alex_dorin в сообщении #752422 писал(а):
Что можно сказать о степени сложности с точки зрения выводимости предложений а Генценовском нормальном выводе ?
Что такое "сложность предложений с точки зрения выводимости в генценовском нормальном выводе"?

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

 
 
 
 Re: О сложности в Генценовском нормальном выводе
Сообщение07.08.2013, 08:39 
Sonic86 в сообщении #752590 писал(а):
Что такое "сложность предложений с точки зрения выводимости в генценовском нормальном выводе"?
Определение приводите, иначе разговор бессмысленен. В Вашем последнем посте определения нет.

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

 
 
 
 Re: О сложности в Генценовском нормальном выводе
Сообщение07.08.2013, 11:25 
alex_dorin в сообщении #752783 писал(а):
К сожалению это сложно. Привожу
Тема: «Логический и сложностной анализ проблем вычислений и теории доказательств».
Номер госрегистрации
01200852829.
Руководитель темы:
доктор физ.-матем. наук
В.П. Оревков
:shock: Вы думаете, мне это что-нибудь скажет?
Не ну если Вы не знаете, о чем у Вас тема (а она о чем-то конкретно), то надо выяснить у научрука.
Если интересует асимптотика работы алгоритма генценовского вывода, то так и напишите и тогда надо алгоритмы смотреть, сколько их там.
Если же Вам надо понятие сложности самому уточнить до какого-то формально точного понятия, то я - пас, надо хотя бы знать, на что Вы или Ваш научрук хотите ориентироваться.

 
 
 
 Re: О сложности в Генценовском нормальном выводе
Сообщение07.08.2013, 11:49 
Аватара пользователя
"Предложение" может быть и невыводимым.
В случае выводимости естественно говорить о минимальной длине выводов, но столь же естественно о времени какого-то алгоритма, находящего выводы.
Первый подход тяготеет к вещам типа колмогоровской/марковксой сложности, второй - к сложности вычислений.
Быть может, ТС пояснит, что он хочет.

 
 
 [ Сообщений: 7 ] 


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group