В работе исследованы сложностные характеристики выводов в системах Фреге и в системах Фреге с правилом подстановки (единичной и мультипликативной). Для произвольной тавтологии φ введено понятие минимально-определяющей дизъюнктивной нормальной формы Ɗ_min (φ) и доказано, что количество шагов кратчайшего вывода тавтологии φ в произвольной системе Фреге не превышает с • s • Ɩ , где s – некая характеристика Ɗ_min (φ), Ɩ —длина формулы φ и с — некоторая константа, зависящая от выбора системы Фреге. При этом указывается, что для произвольного n можно указать последовательность формул длины n, для которых величина s имеет соответственно порядок n, n² , n³ ,…, n^{[√nlog_n 2]} . В работе доказано также, что существует последовательность тавтологий длины n, для которых и в системах Фреге и в системах Фреге с правилом подстановки оценки количества шагов формул и общей длины выводов имеют порядок n и n² соответственно. Доказано также, что существуют тавтологии длины n, выводимые с единичной подстановкой не менее, чем за n шагов, а с мульмультипликативной подстановкой не более, чем за log₂ n шагов.

сложностные характеристики выводов, системы Фреге, системы Фреге с правилом подстановки, определяющий конъюнкт, минимально-определяющая дизъюнктивная нормальная форма

Математические вопросы и теория численных методов