Proof compressions with circuit-structured substitutions

Хорошо известно, что в классическом исчислении высказываний существует экспоненциальный разрыв по величине между “длинными” выводами без сечений (или нормальными выводами) и соответствующими “короткими” выводами с сечениями (или с modus ponens). С другой стороны, задача автоматического поиска вывода обычно решается без существенного использования правила сечения, чтобы разумно ограничить выбор новых секвенций. Однако, как отмечено выше, такое ограничение может привести к экспоненциальному росту искомого вывода. В этом контексте мы предлагаем и обсуждаем методы редукции веса и/или размера выводов посредством замены традиционных древовидных исчислений более либеральными, которыe допускают правила с более чем одним заключением. В работе показано, что использование таких исчислений с правилами подстановки и утончения может дать экспоненциальное ускорение веса и размера выводов даже без правила сечения. Библ. – 10 назв.