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