Две системы доказательства тавтологичности, основанные на методе расщеплений

Рассматриваются два исчисления, где выводимы все пропозициональные тавтологии и только они. Несмотря на простую структуру (каждое из исчислений имеет одну аксиому и одно правило вывода) можно получить линейные оценки длины вывода в них для различных часто встречающихся классов формул, тавтологичность которых распознается в полиномиальное время. Изучаются характеристики формул, влияющие на длину вывода в этих системах. В частности, одной из таких характеристик является степень симметрии, которая определяется автоморфизмами формулы. Библ. – 6 назв.