穷举法
維基百科,自由的 encyclopedia
穷举法,亦称作分类证明、分类分析证明、完全归纳法或暴力法,是一种数学证明方法, 它将所求证的命题分为有限种情形或是等价情形的集合,接著依每种类型分别检验该命题是否成立[1],此乃一种直接证明(英语:direct proof)法。
穷举法证明包括两阶段:
- 证明分类是完全的, 也就是说每一个待证的个例皆符合(至少)一类情形的条件;
- 分别对每一类情形给出证明。
计算机(電腦)的普及大大提升了穷举法的易用性,计算机专家系统可用窮舉法解答許多问题。理论上而言,穷举法适用于任何有限情形,然而因数学的大部分集合是无限的,此法鲜少能够用以导出一般的数学结论[2]。
在柯里-霍华德同构(Curry–Howard correspondence)中,穷举法与ML-型模式匹配相关联[來源請求]。