数値的な証拠・反例・証明

命題 $P$ についての数値計算の結果を、次の 3 つに区別する。

• 数値的な証拠: 有限個の入力について、浮動小数の計算で $P$ と矛盾しない結果を得たこと。$P$ が真であることを含意しない。
• 反例: $P$ が偽であることを示す具体的な入力。ただし浮動小数の計算で見つけた「反例」は、丸め誤差の影響を除く検査（厳密な計算または包含の保証がある計算）を経て初めて反例になる。
• 証明: すべての入力について $P$ が成り立つことの論証。計算機を使う場合は、計算の結果が真の値を含むことが保証された計算（精度保証つき計算。区間演算・球算術・厳密な有理数演算）と、有限個の場合への帰着の論証からなる。