窮舉法
維基百科,自由的 encyclopedia
窮舉法,亦稱作分類證明、分類分析證明、完全歸納法或暴力法,是一種數學證明方法, 它將所求證的命題分為有限種情形或是等價情形的集合,接着依每種類型分別檢驗該命題是否成立[1],此乃一種直接證明(英語:direct proof)法。
窮舉法證明包括兩階段:
- 證明分類是完全的, 也就是說每一個待證的個例皆符合(至少)一類情形的條件;
- 分別對每一類情形給出證明。
計算機(電腦)的普及大大提升了窮舉法的易用性,計算機專家系統可用窮舉法解答許多問題。理論上而言,窮舉法適用於任何有限情形,然而因數學的大部分集合是無限的,此法鮮少能夠用以導出一般的數學結論[2]。
在柯里-霍華德同構(Curry–Howard correspondence)中,窮舉法與ML-型模式匹配相關聯[來源請求]。