モデルと反例

モデルと反例( Mace ) はモデルファインダーです。^{[ 1 ]} ほとんどの自動定理証明器は、証明問題の節標準形に対して反駁による証明を実行しようとします。つまり、公理と否定された予想の組み合わせが同時に真になることは決してない、つまりモデルを持たないことを示します。一方、Mace のようなモデルファインダーは、節の集合の明示的なモデルを見つけようとします。それが成功すれば、これは予想に対する反例に対応し、つまり (主張されている) 定理を反証します。