Фактор Де Брейна
Фактор де Брейна — это мера того, насколько сложнее написать формальное математическое доказательство по сравнению с неформальным . Он был создан голландским пионером компьютерной защиты Николаасом Говертом де Брейном .
Де Брейн вычислил его как размер формального доказательства по сравнению с размером неформального доказательства [ уточнить ] . [1]
Фрик Видейк уточнил определение, чтобы использовать сжатый размер формального доказательства вместо сжатого размера неформального доказательства. Он назвал это «внутренним фактором де Бруйина». Сжатие устраняет эффект, который может иметь длина идентификаторов в доказательствах. [2]
Ссылки
- ^ Видейк, Фрик. «Фактор Де Брёйна». Университет Радбауд . Проверено 11 января 2022 г.
- ^ Видик, Фрик. «Фактор Де Брейна» (PDF) . Университет Радбауд . Проверено 11 января 2022 г.
