The polynomial bounds of proof complexity in Frege systems.
Unsolvable systems of equations and proof complexity.
-tautologies, uniform and non-uniform upper bounds in computation theory
Una -tautologia è una tautologia del tipo avente un solo interpolante di Craig , a meno di equivalenza logica. Utilizzando misure di complessità relative al problema di trovare tale , mostriamo come si possano ottenere limiti non uniformi di complessità mediante limiti uniformi, e viceversa.
Верхние оценки удлинения выводов при устранении сечений
Две системы доказательства тавтологичности, основанные на методе расщеплений
Доказательства в арифметике, использующие случайные числа
Замечание об усилении гипотезы Г.Крайзеля
Импликативная сложность аксиоматик
Нижние оценки увеличения сложности выводов после устранения сечений
О сложности вывода в исчислении высказываний
О сложности линейных выводов в методе резолюций
Рост длины секвенциального вывода при перестройке в натуральный
Сохранение эквивалентности выводов при редукции глубины формул
Схемы доказательств в аксиоматических теориях гильбертовского типа
Теорема когеррентности для канонических морфизмов в декартово замкнутых категориях
Точные оценки доказуемости трансфинитной индукции в начальных отрезках арифметики
Три способа выявления несущественных формул в секвенциях
Упрощение генценовских редукций классической арифметики