Критерий де Брёйна

Критерий де Брёйна — эмпирический критерий надёжности программного обеспечения автоматического доказательства теорем, сформулированный голландским исследователем Николасом де Брёйном.

Инструмент доказательства теорем соответствует критерию де Брёйна, если выходной язык, на котором он генерирует текст доказательства, является небольшим и компактным, даже в том случае, когда система использует сложные и ресурсоемкие процедуры для поиска самого доказательства.

Критерий был сформулирован в качестве компактной формулировки требования обозримости реализации процедур работы инструмента автоматического доказательства теорем. Он подразумевает, что, даже если мы не сможем проверить полностью корректность работы процедур поиска доказательства, у нас должна быть возможность проверить корректность отработки системой автоматически сгенерированного представления самого доказательства и, в том числе, корректность реализации ядра, которое реализует эту отработку. Такая проверка может быть обеспечена, например, таким способом, что скептически настроенный пользователь мог бы самостоятельно написать небольшую программу для проверки одного или нескольких доказательств, сгенерированных инструментом автоматического доказательства теорем, реализуя отработку того же языка представления доказательств, который использует этот инструмент. Подразумевается, что если оба варианта проверки какого-то конкретного доказательства — исходный и со стороны пользователя-скептика отработают одинаково, то это существенно увеличит доверие к качеству реализации исходной системы автоматического доказательства.