Loading article…
de Bruijn 係数は、非公式な数学証明ではなく正式な数学証明を書くのがどれだけ難しいかを示す尺度です。これは、オランダのコンピューター証明の先駆者であるNicolaas Govert de Bruijnによって作成されました。
De Bruijnはそれを、形式的証明のサイズ÷非形式的証明のサイズとして計算した[明確化]。[1]
Freek Wiedijk は、非公式証明の圧縮サイズよりも公式証明の圧縮サイズを使用するように定義を改良しました。彼はこれを「本質的な de Bruijin 係数」と呼びました。圧縮により、証明内の識別子の長さが与える影響がなくなります。[2]
参考文献
- ^ ヴィーダイク、フリーク。 「デ・ブライジン・ファクター」。ラドボウド大学。2022 年1 月 11 日に取得。
- ^ ヴィーディク、フリーク。 「デ・ブライジン・ファクター」(PDF)。ラドバウド大学。2022 年1 月 11 日に取得。