|
ИСТИНА |
Войти в систему Регистрация |
Интеллектуальная Система Тематического Исследования НАукометрических данных |
||
От булевых схем к доказательству теоремстатья
- Автор: Боков Г.В.
- Журнал: Интеллектуальные системы. Теория и приложения (ранее: Интеллектуальные системы по 2014, № 2, ISSN 2075-9460)
- Том: 22
- Номер: 1
- Год издания: 2018
- Издательство: [б.и.]
- Местоположение издательства: М.
- Первая страница: 123
- Последняя страница: 130
- Аннотация: Вопрос о сложности доказательств теорем в формальных системах возникает во многих областях. С точки зрения вычислительной сложности точные нижние оценки сложности доказательств служат средством отделения классов вычислительной сложности. В современных SAT- и SMT-решателях анализ лежащих в их основе систем доказательств позволяет оценить производительность и ограниченность решателей. Центральное место в вопросе сложности доказательств отводится доказательству теорем классического исчисления высказываний. Несмотря на то, что за последние десятилетия удалось разработать много разнообразных техник для доказательства верхних и нижних оценок в различных пропозициональных системах, успеха в получении нижних оценок для классических систем доказательств достичь так и не удалось. Тем не менее, среди специалистов в области сложности доказательств сложилась прочная уверенность в том, что существует тесная связь между прогрессом в получении нижних оценок сложности булевых схем и прогрессом в получении нижних оценок размера пропозициональных доказательств. В работе будет рассказано о связи между булевыми схемами и системами доказательств теорем, о том, как идеи и методы, применяемые для оценки сложности схем, применяются для оценки сложности доказательств теорем.
- Добавил в систему: Боков Григорий Владимирович