Loading AI tools
穷举法，亦称作分类证明、分类分析证明、完全归纳法或暴力法，是一种数学证明方法, 它将所求证的命题分为有限种情形或是等价情形的集合，接著依每种类型分别检验该命题是否成立[1]，此乃一种直接证明法。
穷举法证明包括两阶段：
- 证明分类是完全的, 也就是说每一个待证的个例皆符合（至少）一类情形的条件；
- 分别对每一类情形给出证明。
计算机（電腦）的普及大大提升了穷举法的易用性，计算机专家系统可用窮舉法解答許多问题。理论上而言，穷举法适用于任何有限情形，然而因数学的大部分集合是无限的，此法鲜少能够用以导出一般的数学结论[2]。
在柯里-霍华德同构（Curry–Howard correspondence）中，穷举法与ML-型模式匹配相关联[來源請求]。
试证明每一个完全立方整数皆为9的倍数，或比9的某倍数多1，或比9的某倍数少1。
证明：
- 每个立方数皆为某个整数n的立方。每个整数n或者为3的倍数，或者比3的某个倍数多1或少1。是故以下3种情形即穷举所有可能。
- 情形1: 若 n = 3p, 则 n3 = 27p3, 这是9的倍数.
- 情形2: 若 n = 3p + 1, 则 n3 = 27p3 + 27p2 + 9p + 1, 这是9的一个倍数加上1. 例如, 若 n = 4 则 n3 = 64 = 9×7 + 1.
- 情形3: 若 n = 3p − 1, 则 n3 = 27p3 − 27p2 + 9p − 1, 这是9的一个倍数减去1. 例如, 若 n = 5 则 n3 = 125 = 9×14 − 1.∎
数学家会尽量不用分类数目很多的穷举法, 因为这看上去不优雅. 以下举一个例子来解释何以这样的证明显得不优雅, 这个例子是证明所有现代夏季奥运会的举办年份都能被4整除(忽略掉因两次世界大战而未能举办的1916年夏季奧林匹克運動會,1940年夏季奧林匹克運動會與1944年夏季奧林匹克運動會與受嚴重特殊傳染性肺炎疫情影響，延期至2021年舉辦的2020年夏季奧林匹克運動會)。
证明: 现代首届夏季奥运会于1896年举办, 然后每4年举办一次. 因为 1896 = 474 × 4 能被4整除, 下一届奥运会的年份为 474 × 4 + 4 = (474 + 1) × 4, 同样能被4整除, 以下类推(这个证明用的是数学归纳法). 命题得证.
这个命题也可用穷举法来证, 即列出所有曾举办过夏季奥运会的年份, 核实其皆能被4整除. 到2016年为止, 夏季奥运会共举办过28次, 所以这是一个分了28种情形的穷举证明. 用到数学归纳法的证明不仅更优雅, 且连带对未来无限多次夏季奥运会都证明了命题; 而用穷举法则需在每次开过夏季奥运会之后再做一次核验.
穷举证明中所分情形总数没有上限. 有时只需划分两三种情形, 有些时候却可以有多达数千乃至数百万种情形. 例如, 若要严格解答一个国际象棋残局, 便可能须考察该残局的博弈树中所包含的数量甚巨的允许局面.
四色定理的第一个证明是一个分了1936类情形的穷举证明. 这个证明曾引发争议, 因为其中大多数情形是用计算机程序而不是手写证明来核验. 目前已知最短的四色定理证法仍需划分超过600类情形.
一般而言, 分类的数目越多, 整个证明包含错误的概率就越大. 一个分类数目浩大的穷举证明会给人留下这样的印象, 那就是所证定理能够成立仅仅是一种巧合, 而不是因为某些底层的原理或联系. 其它类型的证明——例如使用数学归纳法的证明——会被认为更加优美. 但是, 有一些重要的定理, 迄今并未发现不用穷举法的证明, 诸如
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
