От булевых схем к доказательству теорем

Вопрос о сложности доказательств теорем в формальных системах возникает во многих областях. С точки зрения вычислительной сложности точные нижние оценки сложности доказательств служат средством отделения классов вычислительной сложности. В современных SAT- и SMT-решателях анализ лежащих в их основе систем доказательств позволяет оценить производительность и ограниченность решателей. Центральное место в вопросе сложности доказательств отводится доказательству теорем классического исчисления высказываний. Несмотря на то, что за последние десятилетия удалось разработать много разнообразных техник для доказательства верхних и нижних оценок в различных пропозициональных системах, успеха в получении нижних оценок для классических систем доказательств достичь так и не удалось. Тем не менее, среди специалистов в области сложности доказательств сложилась прочная уверенность в том, что существует тесная связь между прогрессом в получении нижних оценок сложности булевых схем и прогрессом в получении нижних оценок размера пропозициональных доказательств. В работе будет рассказано о связи между булевыми схемами и системами доказательств теорем, о том, как идеи и методы, применяемые для оценки сложности схем, применяются для оценки сложности доказательств теорем.